test.agda

module test where

open import Reflection
open import Agda.Builtin.Reflection
open import Agda.Builtin.Word
open import Agda.Builtin.Float
open import Agda.Builtin.Char
open import Prelude.List
open import Prelude.Maybe
open import Prelude.Nat
open import Prelude.Ord
open import Prelude.Equality
open import Prelude.Show
open import Prelude.Semiring
open import Prelude.Function
open import Prelude.Unit
open import Prelude.Sum
open import Prelude.Bool
open import Prelude.Product
open import Tactic.Reflection
open import Tactic.Reflection.Equality
open import Tactic.Reflection.DeBruijn
open import Tactic.Reflection.Substitute


pat : Term
pat = pat-lam [ clause [ arg (arg-info visible relevant) (var "ii") ] (def (quote Bool) []) ] [ arg (arg-info visible relevant) (var 0 []) ]



macro
  mm : Term → TC ⊤
  mm hole
    = do
         inContext (arg (arg-info visible relevant) (def (quote Nat) []) ∷ [])
           (do
               t ← reduce pat
               typeError (termErr t ∷ termErr pat ∷ [])
                    )


test : ⊤
test = mm