ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-21 22:17:19 +03:00
Code Issues Projects Releases Wiki Activity

Removes :q alias for :abandon

Browse Source 
As of Idris v0.9.19, :q is no longer accepted by the elab shell.
This commit is contained in:
Jeremy W. Sherman 2015-10-10 20:34:10 -04:00
parent c18bf77285
commit be1183892c
1 changed files with 1 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
docs/reference/elaborator-reflection.rst
View File

@ -81,8 +81,7 @@ to enter the elaboration shell.
The interactive elaboration shell accepts the following commands:
- ``:abandon``, or ``:q`` for short,
quits the elaboration shell, which abandons proving the current lemma.
- ``:abandon`` gives up on proving the current lemma and quits the elaboration shell.
- ``:state`` displays the current state of the term being constructed.