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