Macros
Macros allow you to modify Lambda terms at interpretation time. For example you might want to print out a term, resolve its named terms or reduce/normalize it. Macros are only evaluated once when the term is initially parsed, after that tey are just replaced with the terms they return.
Available Macros:
!cnormalize
- like!normalize
but shows number of reductions performed!debug
- prints out the argument term!macros
- prints available macros!normalize
- reduce the term until it cannot be reduced further (this is the so-called normal form)!reduce
- execute one reduction step on the argument term!resolve
- resolve named terms and church numerals!time
- time the macro execution of term inside!vnormalize
/!vreduce
- like!normalize
and!reduce
, but prints the reduction steps
Examples
[λ] one := \f . \x . f x
one := \f . \x . f x
[λ] !resolve (one y)
(\f . \x . f x) y
[λ] one := \f . \x . f x
one := \f . \x . f x
[λ] !vnormalize (one (\y . y y) z)
one (\y . y y) z
(\x . (\y . y y) x) z
(\x . x x) z
z z