git.iko.soy/Idris-dev
on master help sign in
Remove advice to import Language.Reflection.Elab

This no longer applies as of HEAD, as pointed out by @david-christiansen, because the Prelude now includes this namespace. Replace the advice with a tip to :browse the Tactics module to see the list of tactics prior to entering the elab shell.

commitd75e4c6d299e5ad73b70599dc8bcefd8b68dbe1b authorJeremy W. Sherman <jeremyw.sherman@gmail.com> dateMon 12 Oct 2015, 18:27 (11 years ago) parentc6c4bf4
1 file changed+2−3
compare with master
unifiedsplit
docs/reference/elaborator-reflection.rst+2−3
docs/reference/elaborator-reflection.rst+2−3
@@ -80,9 +80,8 @@ Then, issue the ``:elab <hole>`` command at the REPL
8080to enter the elaboration shell.
8181
8282At the shell, you can enter proof tactics to alter the proof state.
83−It is recommended to issue ``:module Language.Reflection.Elab``
84−prior to entering the elaboration shell in order to have the system-provided
85−tactics available to you.
83+You can view the system-provided tactics prior to entering the shell
84+by issuing the REPL command ``:browse Language.Reflection.Elab.Tactics``.
8685When you have discharged all goals, you can complete the proof
8786using the ``:qed`` command and receive in return an elaboration script
8887that fills the hole.