@@ -88,7 +88,9 @@ that fills the hole.
89The interactive elaboration shell accepts a limited number of commands,
89The interactive elaboration shell accepts a limited number of commands,
90including a subset of the commands understood by the normal Idris REPL
90including a subset of the commands understood by the normal Idris REPL
91−as well as some elaboration-specific commands.
91+as well as some elaboration-specific commands. It also supports the
92+``do``-syntax, meaning you can write ``res <- command`` to bind the result of
93+``command`` to variable ``res``.
93General-purpose commands:
95General-purpose commands: