@@ -74,17 +74,53 @@ We can generate identity functions at any concrete type using the same script:
74Interactively Building Elab Scripts
74Interactively Building Elab Scripts
75===================================
75===================================
77−To build an ``Elab`` script interactively, use the ``:elab`` command at the REPL.
77+You can build an ``Elab`` script interactively at the REPL.
78−It takes the name of a hole as an argument.
78+Use the command ``:metavars``, or ``:m`` for short, to list the available holes.
79−To list all available holes, use the command ``:m``.
79+Then, issue the ``:elab <hole>`` command at the REPL
80−
80+to enter the elaboration shell.
82+At the shell, you can enter proof tactics to alter the proof state.
83+You can view the system-provided tactics prior to entering the shell
84+by issuing the REPL command ``:browse Language.Reflection.Elab.Tactics``.
85+When you have discharged all goals, you can complete the proof
86+using the ``:qed`` command and receive in return an elaboration script
81−In interactive elaboration shell, the following commands are available:
89+The interactive elaboration shell accepts a limited number of commands,
82−- ``:q`` - Quits the elaboration shell (gives up on proving current lemma).
90+including a subset of the commands understood by the normal Idris REPL
83−- ``:abandon`` - Same as :q
91+as well as some elaboration-specific commands.
93+General-purpose commands:
95+- ``:eval <EXPR>``, or ``:e <EXPR>`` for short, evaluates the provided expression
96+ and prints the result.
98+- ``:type <EXPR>``, or ``:t <EXPR>`` for short, prints the provided expression
99+ together with its type.
101+- ``:search <TYPE>`` searches for definitions having the provided type.
103+- ``:doc <NAME>`` searches for definitions with the provided name and prints their
107+Commands for viewing the proof state:
84−- ``:state`` - Displays the current state of the term being constructed.
109+- ``:state`` displays the current state of the term being constructed. It lists both
110+ other goals and the current goal.
85−- ``:term`` - Displays the current proof term complete with its yet-to-be-filled holes.
112+- ``:term`` displays the current proof term as well as its yet-to-be-filled holes.
115+Commands for manipulating the proof state:
86−- ``:undo`` - Undoes the last tactic.
117+- ``:undo`` undoes the effects of 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)
118+
119+- ``:abandon`` gives up on proving the current lemma and quits the elaboration shell.
121+- ``:qed`` finishes the script and exits the elaboration shell. The shell will only accept
122+ this command once it reports, "No more goals." On exit, it will print out the finished
123+ elaboration script for you to copy into your program.