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 ;.