REPL

Right now, calling it a REPL is an overstatement: it's a read-typecheck-print-loop, but that's the important part. An expression or declaration typed into the command line will type-check the term, print the type and, ind the case of a declaration, add the binding to the environment. In addition, there's several commands:

• :load "filename" — loads the definitions from filename. Quotes are mandatory (sorry).
• :showAll — print the types of all the holes in the currently read program
• :show [n] — show the typing context and the type of the n-th hole. The variant without any number is only valid if focused
• :focus n — focus on the n-th hole
• :unfocus — just what it says on the tin
• :refine [n] expr — fill in the n-th hole with the expression expr. As with show, if focused, the number can be omitted.
• :apply [n] expr — apply the expression to the (n-th or focused) hole. This command tries to match the type of the hole with the type of expr and, if expr requires extra arguments to match the type, leaves the appropriate number of holes. For example, if foo : A -> B -> C, and the type of the hole is B -> C, the tactic will generate one hole of type A.
• :case [n] expr — refine the hole with a case-expression using expr as the splitting term. All the alternatives are generated, each with a new hole.
• :clear — reset the whole environment of the REPL (declarations and holes).

At this time, the best idea is to run the REPL, load up the code from "examples/stuff.esml" file, and play with refining/applying stuff to see how it works.