@@ -11,11 +11,6 @@ For details, see Edwin Brady's 2013 paper in the Journal of Functional Programmi
1111Elaborator reflection makes the elaboration type as well as a selection of its tactics available to Idris code.
1212This means that metaprograms written in Idris can have complete control over the elaboration process, generating arbitrary code, and they have access to all of the facilities available in the elaborator, such as higher-order unification, type checking, and emitting auxiliary definitions.
1313
14−WARNING
15−=======
16−
17−Elaborator reflection is a new, **experimental** feature. It **will change**. You've been warned.
18−
1914The Elaborator State
2015====================
2116
@@ -81,8 +76,15 @@ Interactively Building Elab Scripts
8176
8277To build an ``Elab`` script interactively, use the ``:elab`` command at the REPL.
8378It takes the name of a hole as an argument.
84−The interface is largely the same as in Idris's interactive prover, except all meta-commands start with colon.
85−For example, use ``:qed`` instead of ``qed``, ``:abandon`` instead of ``abandon``, and ``:undo`` instead of ``undo``.
79+To list all available holes, use the command ``:m``.
80+
81+In interactive elaboration shell, the following commands are available:
82+- ``:q`` - Quits the elaboration shell (gives up on proving current lemma).
83+- ``:abandon`` - Same as :q
84+- ``:state`` - Displays the current state of the term being constructed.
85+- ``:term`` - Displays the current proof term complete with its yet-to-be-filled holes.
86+- ``:undo`` - Undoes the last tactic.
87+- ``:qed`` - Once the elaboration shell tells you "No more goals," you get to type this in celebration! (Completes the construction and exits the shell)
8688
8789
8890Failure