Agda gives a parse error when trying to use both tactic and irrelevant annotation.
module Test where
open import Agda.Builtin.Bool
open import Agda.Builtin.Unit
open import Agda.Builtin.Reflection
defaultTo : {A : Set} (x : A) → Term → TC ⊤
defaultTo x hole = bindTC (quoteTC x) (unify hole)
--works
f : {@(tactic defaultTo true) x : Bool} → Bool
f {x} = x
--works
g : {@irr @(tactic defaultTo true) x : Bool} → Bool
g = true
{-
error: [ParseError]
:<ERROR> Bool} → Bool
h = true
...
-}
h : .{ @(tactic defaultTo true) x : Bool} → Bool
h = true
Agda version :
Agda version 2.8.0-f9f2714
Built with flags (cabal -f)
- optimise-heavily: extra optimisations
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4