@@ -79,17 +79,47 @@ Use the command ``:metavars``, or ``:m`` for short, to list the available holes.
7979Then, issue the ``:elab <hole>`` command at the REPL
8080to enter the elaboration shell.
8181
82−The interactive elaboration shell accepts the following commands:
82+At the shell, you can enter proof tactics to alter the proof state.
83+It is recommended to issue ``:module Language.Reflection.Elab``
84+prior to entering the elaboration shell in order to have the system-provided
85+tactics available to you.
86+When you have discharged all goals, you can complete the proof
87+using the ``:qed`` command and receive in return an elaboration script
88+that fills the hole.
8389
84−- ``:abandon`` gives up on proving the current lemma and quits the elaboration shell.
90+The interactive elaboration shell accepts a limited number of commands,
91+including a subset of the commands understood by the normal Idris reply
92+as well as some elaboration-specific commands.
93+
94+General-purpose commands that remain available in the elaboration shell:
95+
96+- ``:eval <EXPR>``, or ``:e <EXPR>`` for short, evaluates the provided expression
97+ and prints the result.
98+
99+- ``:type <EXPR>``, or ``:t <EXPR>`` for short, prints the provided expression
100+ together with its type.
101+
102+- ``:search <TYPE>`` searches for definitions having the provided type.
103+
104+- ``:doc <NAME>`` searches for definitions with the provided name and prints their
105+ documentation.
85106
86−- ``:state`` displays the current state of the term being constructed.
87107
88−- ``:term`` displays the current proof term as well as its yet-to-be-filled holes.
108+Commands for viewing the proof state:
89109
90−- ``:undo`` undoes the last tactic.
110+- ``:state`` displays the current state of the term being constructed. It lists both
111+ other goals and the current goal.
112+
113+- ``:term`` displays the current proof term as well as its yet-to-be-filled holes.
114+
115+
116+Commands for manipulating the manipulating the proof state:
117+
118+- ``:undo`` undoes the effects of the last tactic.
119+
120+- ``:abandon`` gives up on proving the current lemma and quits the elaboration shell.
91121
92−- ``:qed`` finishes the script and exits the elaboration shell. The shell will only accept
122+- ``:qed`` finishes the script and exits the elaboration shell. The shell will only accept
93123 this command once it reports, "No more goals." On exit, it will print out the finished
94124 elaboration script for you to copy into your program.
95125