mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-19 09:12:34 +03:00
23 lines
470 B
Idris
23 lines
470 B
Idris
module QuoteSearch
|
|
|
|
import Language.Reflection
|
|
|
|
%language ElabReflection
|
|
|
|
x : Elab Nat
|
|
x = check `(%search)
|
|
|
|
defy : Elab ()
|
|
defy = do
|
|
let fc = EmptyFC
|
|
|
|
val <- quote !x
|
|
logTerm "" 0 "Quoted term:" val
|
|
|
|
declare [
|
|
IClaim fc MW Private [] (MkTy fc fc (UN (Basic "y")) (IVar fc (UN (Basic "Nat")))),
|
|
IDef fc (UN (Basic "y")) [PatClause fc (IVar fc (UN (Basic "y"))) (IApp fc (IApp fc (IVar fc (UN (Basic "+"))) val) val)]
|
|
]
|
|
|
|
%runElab defy
|