mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-21 10:18:23 +03:00
2a75731916
So the type of Elab now gives the expected type that's being elaborated to, meaning that we can run 'check' in the middle of scripts and use the result.
22 lines
589 B
Idris
22 lines
589 B
Idris
import Language.Reflection
|
|
|
|
%language ElabReflection
|
|
|
|
logDecls : TTImp -> Elab (Int -> Int)
|
|
logDecls v
|
|
= do declare [IClaim EmptyFC MW Public []
|
|
(MkTy EmptyFC `{{ Main.foo }}
|
|
`(Int -> Int -> Int) )]
|
|
|
|
declare `[ foo x y = x + y ]
|
|
|
|
declare `[ multBy : Int -> Int
|
|
multBy x = x * ~(v) ]
|
|
declare `[ myplus : Nat -> Nat -> Nat
|
|
myplus Z y = y
|
|
myplus (S k) y = S (myplus k y) ]
|
|
check `( multBy )
|
|
|
|
mkMult : Int -> Int
|
|
mkMult = %runElab logDecls `(4)
|