@@ -74,17 +74,53 @@ We can generate identity functions at any concrete type using the same script:
7474Interactively Building Elab Scripts
7575===================================
7676
77−To build an ``Elab`` script interactively, use the ``:elab`` command at the REPL.
78−It takes the name of a hole as an argument.
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)
77+You can build an ``Elab`` script interactively at the REPL.
78+Use the command ``:metavars``, or ``:m`` for short, to list the available holes.
79+Then, issue the ``:elab <hole>`` command at the REPL
80+to enter the elaboration shell.
81+
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
87+that fills the hole.
88+
89+The interactive elaboration shell accepts a limited number of commands,
90+including a subset of the commands understood by the normal Idris REPL
91+as well as some elaboration-specific commands.
92+
93+General-purpose commands:
94+
95+- ``:eval <EXPR>``, or ``:e <EXPR>`` for short, evaluates the provided expression
96+ and prints the result.
97+
98+- ``:type <EXPR>``, or ``:t <EXPR>`` for short, prints the provided expression
99+ together with its type.
100+
101+- ``:search <TYPE>`` searches for definitions having the provided type.
102+
103+- ``:doc <NAME>`` searches for definitions with the provided name and prints their
104+ documentation.
105+
106+
107+Commands for viewing the proof state:
108+
109+- ``:state`` displays the current state of the term being constructed. It lists both
110+ other goals and the current goal.
111+
112+- ``:term`` displays the current proof term as well as its yet-to-be-filled holes.
113+
114+
115+Commands for manipulating the proof state:
116+
117+- ``:undo`` undoes the effects of the last tactic.
118+
119+- ``:abandon`` gives up on proving the current lemma and quits the elaboration shell.
120+
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.
88124
89125
90126Failure