Fix typo: reply -> REPL
Thanks to @david-christiansen for catching this.
commitf30db6b227b2bbc8f203afdfa75aacba797b21c9
authorJeremy W. Sherman <jeremyw.sherman@gmail.com>
dateMon 12 Oct 2015, 18:19 (11 years ago)
parent6a7b071
docs/reference/elaborator-reflection.rst+1−1
@@ -88,7 +88,7 @@ using the ``:qed`` command and receive in return an elaboration script
8888that fills the hole.
8989
9090The 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
9292as well as some elaboration-specific commands.
9393
9494General-purpose commands that remain available in the elaboration shell: