Skip to content

Instantly share code, notes, and snippets.

@UlfNorell
Last active August 29, 2015 14:20
Show Gist options
  • Save UlfNorell/bc160a5d84fa51c255ba to your computer and use it in GitHub Desktop.
Save UlfNorell/bc160a5d84fa51c255ba to your computer and use it in GitHub Desktop.
open import Prelude
open import Builtin.Reflection
open import Tactic.Reflection.Quote
data TTerm {a} (A : Set a) : Set where
typed : Term → TTerm A
mkTyped : ∀ {a} {A : Set a} → A → Term → TTerm A
mkTyped _ t = typed t
macro
quote-typed : Term → Term
quote-typed t = def (quote mkTyped) (vArg t ∷ vArg (` t) ∷ [])
foo : TTerm Nat
foo = quote-typed (5 ofType Nat)
macro
unquote-typed : Term → Term
unquote-typed (con (quote typed) (_ ∷ _ ∷ vArg t ∷ [])) = unquote-term t []
unquote-typed _ = unknown
bar : Nat
bar = unquote-typed foo
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment