62bb361 · Idris-dev · git.iko.soy

docs/effects/hangman.rst+1−1

compare with master

unifiedsplit

@@ -265,7 +265,7 @@ generator, then pick a random ``Fin`` to index into a list of

265

266.. note::

267 Rather than have to explicitly declare a type with the vector’s

268− length, it is convenient to give a metavariable ``?wtype`` and let

268+ length, it is convenient to give a hole ``?wtype`` and let

269 Idris’s proof search mechanism find the type. This is a

270 limited form of type inference, but very useful in practice.

271

docs/guides/theorem-prover.rst+1−1

@@ -36,7 +36,7 @@ Explore the Context

36====================

37

38We start the interactive session by asking Idris to prove the

39−metavaraible ``rhs`` using the command ``:p rhs``. Idris by default

39+hole ``rhs`` using the command ``:p rhs``. Idris by default

40will show us the initial context. This looks as follows::

41

42 *Foo> :p rhs

docs/proofs/interactive.rst+6−6

@@ -17,7 +17,7 @@ Consider the following definition, proved in :ref:`sect-theorems`:

17

18We’ll be constructing the proof by *induction*, so we write the cases for ``Z``

19and ``S``, with a recursive call in the ``S`` case giving the inductive

20−hypothesis, and insert *metavariables* for the rest of the definition:

20+hypothesis, and insert *holes* for the rest of the definition:

21

22.. code-block:: idris

23

@@ -28,14 +28,14 @@ hypothesis, and insert *metavariables* for the rest of the definition:

28

29On running , two global names are created, ``plusredZ_Z`` and

30``plusredZ_S``, with no definition. We can use the ``:m`` command at the

31−prompt to find out which metavariables are still to be solved (or, more

31+prompt to find out which holes are still to be solved (or, more

32precisely, which functions exist but have no definitions), then the

33``:t`` command to see their types:

34

35.. code-block:: idris

36

37 *theorems> :m

38− Global metavariables:

38+ Global holes:

39 [plusredZ_S,plusredZ_Z]

40

41.. code-block:: idris

@@ -81,8 +81,8 @@ introduces subgoals for each of the function’s explicit arguments

81Here, we could also have used the ``trivial`` tactic, which tries to

82refine by ``Refl``, and if that fails, tries to refine by each name in

83the local context. When a proof is complete, we use the ``qed`` tactic

84−to add the proof to the global context, and remove the metavariable from

84+to add the proof to the global context, and remove the hole from the

85−the unsolved metavariables list. This also outputs a trace of the proof:

85+unsolved holes list. This also outputs a trace of the proof:

86

87.. code-block:: idris

88

@@ -94,7 +94,7 @@ the unsolved metavariables list. This also outputs a trace of the proof:

94.. code-block:: idris

95

96 *theorems> :m

97− Global metavariables:

97+ Global holes:

98 [plusredZ_S]

99

100The ``:addproof`` command, at the interactive prompt, will add the proof

docs/proofs/patterns.rst+6−6

@@ -14,13 +14,13 @@ mapping to Emacs commands.

14+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+

16+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+

18+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+

20+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+

22+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+

24+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+

26+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+

@@ -56,7 +56,7 @@ should see:

56 plus_commutes Z m = ?plus_commutes_rhs_1

57 plus_commutes (S k) m = ?plus_commutes_rhs_2

58

59−If we inspect the types of the newly created metavariables,

59+If we inspect the types of the newly created holes,

60``plus_commutes_rhs_1`` and ``plus_commutes_rhs_2``, we see that the

61type of each reflects that ``n`` has been refined to ``Z`` and ``S k``

62in each respective case. Pressing ``\t`` over

@@ -102,7 +102,7 @@ yields:

102 plus_commutes Z m = plus_commutes_Z

103 plus_commutes (S k) m = ?plus_commutes_S

104

105−That is, the metavariable has been filled with a call to a top level

105+That is, the hole has been filled with a call to a top level

106function ``plus_commutes_Z``. The argument ``m`` has been made implicit

107because it can be inferred from context when it is applied.

108

@@ -334,7 +334,7 @@ defined by matching on its first argument. The complete definition is:

334 plus_commutes_S k Z = Refl

335 plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl

336

337−All metavariables have now been solved.

337+All holes have now been solved.

338

339The ``total`` annotation means that we require the final function to

340pass the totality checker; i.e. it will terminate on all possible

docs/reference/elaborator-reflection.rst+1−1

@@ -78,7 +78,7 @@ Interactively Building Elab Scripts

78===================================

79

80To build an ``Elab`` script interactively, use the ``:elab`` command at the REPL.

81−It takes the name of a metavariable as an argument.

81+It takes the name of a hole as an argument.

82The interface is largely the same as in Idris's interactive prover, except all meta-commands start with colon.

83For example, use ``:qed`` instead of ``qed``, ``:abandon`` instead of ``abandon``, and ``:undo`` instead of ``undo``.

84

docs/reference/ide-protocol.rst+2−2

@@ -78,14 +78,14 @@ The available commands include:

78 The new code is returned with no highlighting.

79

80 ``(:proof-search LINE NAME HINTS)``

81− Attempt to fill out the metavariable on ``LINE```named ``NAME`` by proof search.

81+ Attempt to fill out the holes on ``LINE```named ``NAME`` by proof search.

82 ``HINTS`` is a possibly-empty list of additional things to try while searching.

83

84 ``(:docs-for NAME)``

85 Look up the documentation for ``NAME``, and return it as a highlighted string.

86

87 ``(:metavariables WIDTH)``

88− List the currently-active metavariables, with their types pretty-printed with ``WIDTH`` columns.

88+ List the currently-active holes, with their types pretty-printed with ``WIDTH`` columns.

89

90 ``(:who-calls NAME)``

91 Get a list of callers of ``NAME``

docs/reference/repl.rst+2−2

@@ -104,9 +104,9 @@ The current set of supported commands are:

104+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

105|:e :edit | | Edit current file using $EDITOR or $VISUAL |

106+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

107−|:m :metavars | | Show remaining proof obligations (metavariables) |

107+|:m :metavars | | Show remaining proof obligations (holes) |

108+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

109−|:p :prove | <metavar> | Prove a metavariable |

109+|:p :prove | <hole> | Prove a hole |

110+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

111|:a :addproof | <name> | Add proof to source file |

112+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

docs/reference/tactics.rst+6−6

@@ -2,12 +2,12 @@

2Tactics and Theorem Proving

3***************************

4

5−Idris supports interactive theorem proving, and theh analyse of

5+Idris supports interactive theorem proving, and the analyse of context

6−context through metavariables. To list all unproven metavariables,

6+through holes. To list all unproven holes, use the command ``:m``.

7−use the command ``:m``. This will display their qualified names and

7+This will display their qualified names and the expected types. To

8−the expected types. To interactively prove a metavariable, use the

8+interactively prove a holes, use the command ``:p name`` where ``name``

9−command ``:p name`` where ``name`` is the metavariable. Once the proof

10−is complete, the command ``:a`` will append it to the current module.

9+is the hole. Once the proof is complete, the command ``:a`` will append

10+it to the current module.

11

12Once in the interactive prover, the following commands are available:

13

docs/tutorial/interactive.rst+6−6

@@ -16,7 +16,7 @@ are *correct by construction*.

16The Idris REPL provides several commands for inspecting and

17modifying parts of programs, based on their types, such as case

18splitting on a pattern variable, inspecting the type of a

19−metavariable, and even a basic proof search mechanism. In this

19+hole, and even a basic proof search mechanism. In this

20section, we explain how these features can be exploited by a text

21editor, and specifically how to do so in `Vim

22<https://github.com/idris-hackers/idris-vim>`_. An interactive mode

@@ -151,10 +151,10 @@ lead to unification errors.

151------------

152

153The ``:proofsearch n f`` command, abbreviated ``:ps n f``, attempts to

154−find a value for the metavariable ``f`` on line ``n`` by proof search,

154+find a value for the hole ``f`` on line ``n`` by proof search,

155trying values of local variables, recursive calls and constructors of

156the required family. Optionally, it can take a list of *hints*, which

157−are functions it can try applying to solve the metavariable. For

157+are functions it can try applying to solve the hole. For

158example, if the code beginning on line 94 is:

159

160.. code-block:: idris

@@ -237,16 +237,16 @@ each of which update the buffer directly:

237

238- ``\w`` adds a ``with`` clause (using ``:makewith``).

239

240−- ``\o`` invokes a proof search to solve the metavariable under the

240+- ``\o`` invokes a proof search to solve the hole under the

241 cursor (using ``:proofsearch``).

242

243- ``\p`` invokes a proof search with additional hints to solve the

244− metavariable under the cursor (using ``:proofsearch``).

244+ hole under the cursor (using ``:proofsearch``).

245

246There are also commands to invoke the type checker and evaluator:

247

248- ``\t`` displays the type of the (globally visible) name under the

249− cursor. In the case of a metavariable, this displays the context

249+ cursor. In the case of a hole, this displays the context

250 and the expected type.

251

252- ``\e`` prompts for an expression to evaluate.

docs/tutorial/provisional.rst+2−2

@@ -81,14 +81,14 @@ definitions, except that they introduce the right hand side with a

81 parity (S (S (S (j + j)))) | Odd ?= Odd {n=S j}

82

83When written in this form, instead of reporting a type error, Idris

84−will insert a metavariable standing for a theorem which will correct the

84+will insert a hole standing for a theorem which will correct the

85type error. Idris tells us we have two proof obligations, with names

86generated from the module and function names:

87

88.. code-block:: idris

89

90 *views> :m

91− Global metavariables:

91+ Global holes:

92 [views.parity_lemma_2,views.parity_lemma_1]

93

94The first of these has the following type: