Expressions E
:
^ x y .. z . E
\ x y .. z . E
E₁ E₂
Commands:
E
– evaluate expression E
x := E
– define x
:constant x
– declare constant x
:context
– print current context
:lazy
– lazy evaluation
:eager
– eager evaluation
:deep
– evaluate inside λ-abstractions
:shallow
– only evaluate top level
In a file commands must be separated with ;
.