Removes :q alias for :abandon
As of Idris v0.9.19, :q is no longer accepted by the elab shell.
commitbe1183892ce5bfde6ed164e38de7a954fa670646
authorJeremy W. Sherman <jeremyw.sherman@gmail.com>
dateSat 10 Oct 2015, 20:34 (11 years ago)
parentc18bf77
docs/reference/elaborator-reflection.rst+1−2
@@ -81,8 +81,7 @@ to enter the elaboration shell.
8181
8282The interactive elaboration shell accepts the following commands:
8383
84−- ``:abandon``, or ``:q`` for short,
85− quits the elaboration shell, which abandons proving the current lemma.
84+- ``:abandon`` gives up on proving the current lemma and quits the elaboration shell.
8685
8786- ``:state`` displays the current state of the term being constructed.
8887