Drop claim that general-purpose commands are general REPL commands
:e at least is not, as pointed out by @david-christiansen.
commitc6c4bf4688a135d2a992e9dda93a34d62c484c1a
authorJeremy W. Sherman <jeremyw.sherman@gmail.com>
dateMon 12 Oct 2015, 18:21 (11 years ago)
parentd17f246
docs/reference/elaborator-reflection.rst+1−1
@@ -91,7 +91,7 @@ The interactive elaboration shell accepts a limited number of commands,
9191including a subset of the commands understood by the normal Idris REPL
9292as well as some elaboration-specific commands.
9393
94−General-purpose commands that remain available in the elaboration shell:
94+General-purpose commands:
9595
9696- ``:eval <EXPR>``, or ``:e <EXPR>`` for short, evaluates the provided expression
9797 and prints the result.