git.iko.soy/Idris-dev
on master help sign in
Fix typo: reply -> REPL
f30db6bJeremy W. Sherman
docs/reference/elaborator-reflection.rst+1−1
compare with master
unifiedsplit
@@ -88,7 +88,7 @@ using the ``:qed`` command and receive in return an elaboration script
88that fills the hole.
88that fills the hole.
89
89
90The interactive elaboration shell accepts a limited number of commands,
90The interactive elaboration shell accepts a limited number of commands,
91−including a subset of the commands understood by the normal Idris reply
91+including a subset of the commands understood by the normal Idris REPL
92as well as some elaboration-specific commands.
92as well as some elaboration-specific commands.
93
93
94General-purpose commands that remain available in the elaboration shell:
94General-purpose commands that remain available in the elaboration shell: