@@ -88,7 +88,9 @@ that fills the hole.
8888
8989The interactive elaboration shell accepts a limited number of commands,
9090including 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``.
9294
9395General-purpose commands:
9496