| 123456789101112131415161718 |
- open import Agda.Builtin.List
- open import Agda.Builtin.Reflection
- open import Agda.Builtin.Unit
- postulate
- A B : Set
- @0 a : A
- tac : Term → TC ⊤
- tac = unify (def (quote a) [])
- postulate
- f : {@0 @(tactic tac) x : A} → B
- test : B
- test = f
|
