git.iko.soy/Idris-dev
on master help sign in
Update tactics documentation based on deprecation
8a1bc7dDavid Raymond Christiansen
docs/reference/elaborator-reflection.rst+9−7
compare with master
unifiedsplit
@@ -11,11 +11,6 @@ For details, see Edwin Brady's 2013 paper in the Journal of Functional Programmi
11Elaborator reflection makes the elaboration type as well as a selection of its tactics available to Idris code.
11Elaborator reflection makes the elaboration type as well as a selection of its tactics available to Idris code.
12This means that metaprograms written in Idris can have complete control over the elaboration process, generating arbitrary code, and they have access to all of the facilities available in the elaborator, such as higher-order unification, type checking, and emitting auxiliary definitions.
12This means that metaprograms written in Idris can have complete control over the elaboration process, generating arbitrary code, and they have access to all of the facilities available in the elaborator, such as higher-order unification, type checking, and emitting auxiliary definitions.
13
13
14−WARNING
15−=======
16−
17−Elaborator reflection is a new, **experimental** feature. It **will change**. You've been warned.
18−
19The Elaborator State
14The Elaborator State
20====================
15====================
21
16
@@ -81,8 +76,15 @@ Interactively Building Elab Scripts
81
76
82To build an ``Elab`` script interactively, use the ``:elab`` command at the REPL.
77To build an ``Elab`` script interactively, use the ``:elab`` command at the REPL.
83It takes the name of a hole as an argument.
78It takes the name of a hole as an argument.
84−The interface is largely the same as in Idris's interactive prover, except all meta-commands start with colon.
79+To list all available holes, use the command ``:m``.
85−For example, use ``:qed`` instead of ``qed``, ``:abandon`` instead of ``abandon``, and ``:undo`` instead of ``undo``.
80+
81+In interactive elaboration shell, the following commands are available:
82+- ``:q`` - Quits the elaboration shell (gives up on proving current lemma).
83+- ``:abandon`` - Same as :q
84+- ``:state`` - Displays the current state of the term being constructed.
85+- ``:term`` - Displays the current proof term complete with its yet-to-be-filled holes.
86+- ``:undo`` - Undoes the last tactic.
87+- ``:qed`` - Once the elaboration shell tells you "No more goals," you get to type this in celebration! (Completes the construction and exits the shell)
86
88
87
89
88Failure
90Failure
docs/reference/tactics.rst+10−6
@@ -1,7 +1,11 @@
1***************************
1***************************
2−Tactics and Theorem Proving
2+DEPRECATED: Tactics and Theorem Proving
3***************************
3***************************
4
4
5+.. warning::
6+ The interactive theorem-proving interface documented here has been
7+ deprecated in favor of :ref:`elaborator-reflection`.
8+
5Idris supports interactive theorem proving, and the analyse of context
9Idris supports interactive theorem proving, and the analyse of context
6through holes. To list all unproven holes, use the command ``:m``.
10through holes. To list all unproven holes, use the command ``:m``.
7This will display their qualified names and the expected types. To
11This will display their qualified names and the expected types. To
@@ -15,12 +19,12 @@ Basic commands
15==============
19==============
16
20
17- ``:q`` - Quits the prover (gives up on proving current lemma).
21- ``:q`` - Quits the prover (gives up on proving current lemma).
18−- ``abandon`` - Same as :q
22+- ``:abandon`` - Same as :q
19−- ``state`` - Displays the current state of the proof.
23+- ``:state`` - Displays the current state of the proof.
20−- ``term`` - Displays the current proof term complete with its
24+- ``:term`` - Displays the current proof term complete with its
21 yet-to-be-filled holes (is only really useful for debugging).
25 yet-to-be-filled holes (is only really useful for debugging).
22−- ``undo`` - Undoes the last tactic.
26+- ``:undo`` - Undoes the last tactic.
23−- ``qed`` - Once the interactive theorem prover tells you "No more
27+- ``:qed`` - Once the interactive theorem prover tells you "No more
24 goals," you get to type this in celebration! (Completes the proof and
28 goals," you get to type this in celebration! (Completes the proof and
25 exits the prover)
29 exits the prover)
26
30