test.agda

module test where

open import Agda.Builtin.Reflection
open import Reflection
open import Prelude.Nat
open import Prelude.Bool
open import Prelude.Unit
open import Prelude.List


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