mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-16 07:34:45 +03:00
d5b5af91d1
A %macro must always be fully applied. Whenever the elaborator encounters a %macro application (except in a function LHS) it evaluates the application and sends the result to %runElab. So: %macro foo : args -> Elab TT ... def = foo a b c is equivalent to foo : args -> Elab TT ... def = %runElab foo a b c
15 lines
242 B
Idris
15 lines
242 B
Idris
import Language.Reflection
|
|
|
|
%language ElabReflection
|
|
|
|
powerFn : Nat -> TTImp
|
|
powerFn Z = `(const 1)
|
|
powerFn (S k) = `(\x => mult x (~(powerFn k) x))
|
|
|
|
%macro
|
|
power : Nat -> Elab TT
|
|
power n = check (powerFn n)
|
|
|
|
cube : Nat -> Nat
|
|
cube = power 3
|