@@ -74,18 +74,25 @@ 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.
81−In interactive elaboration shell, the following commands are available:
82+The interactive elaboration shell accepts the following commands:
84+- ``:abandon``, or ``:q`` for short,
83−- ``:q`` - Quits the elaboration shell (gives up on proving current lemma).
85+ quits the elaboration shell, which abandons proving the current lemma.
84−- ``:abandon`` - Same as :q
86+
85−- ``:state`` - Displays the current state of the term being constructed.
87+- ``:state`` displays the current state of the term being constructed.
86−- ``:term`` - Displays the current proof term complete with its yet-to-be-filled holes.
89+- ``:term`` displays the current proof term as well as its yet-to-be-filled holes.
87−- ``:undo`` - Undoes the last tactic.
91+- ``:undo`` undoes the last tactic.
88−- ``:qed`` - Once the elaboration shell tells you "No more goals," you get to type this in celebration! (Completes the construction and exits the shell)
92+
93+- ``:qed`` finishes the script and exits the elaboration shell. The shell will only accept
94+ this command once it reports, "No more goals." On exit, it will print out the finished
95+ elaboration script for you to copy into your program.