696f336 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Replace "metavariable" with "hole"

commit696f336096b548f9a124af00fad6ad86c1bda11c authorMichael Gilliland <mjg.py3@gmail.com> dateTue 30 Jun 2015, 20:31 (11 years ago) parent4f8d10f

10 files changed+33−33

compare with master

unifiedsplit

docs/effects/hangman.rst+1−1 docs/guides/theorem-prover.rst+1−1 docs/proofs/interactive.rst+6−6 docs/proofs/patterns.rst+6−6 docs/reference/elaborator-reflection.rst+1−1 docs/reference/ide-protocol.rst+2−2 docs/reference/repl.rst+2−2 docs/reference/tactics.rst+6−6 docs/tutorial/interactive.rst+6−6 docs/tutorial/provisional.rst+2−2

docs/effects/hangman.rst+1−1

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

262262

263263.. note::

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

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

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

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

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

268268

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

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

3636====================

3737

3838We 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

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

4141

4242 *Foo> :p rhs

docs/proofs/interactive.rst+6−6

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

1717

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

1919and ``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:

2121

2222.. code-block:: idris

2323

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

2828

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

3030``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

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

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

3434

3535.. code-block:: idris

3636

3737 *theorems> :m

38− Global metavariables:

38+ Global holes:

3939 [plusredZ_S,plusredZ_Z]

4040

4141.. code-block:: idris

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

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

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

8383the 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

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

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

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

8686

8787.. code-block:: idris

8888

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

9494.. code-block:: idris

9595

9696 *theorems> :m

97− Global metavariables:

97+ Global holes:

9898 [plusredZ_S]

9999

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

docs/proofs/patterns.rst+6−6

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

1414+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+

1616+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+

1818+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+

2020+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+

2222+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+

2424+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+

2626+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+

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

5656 plus_commutes Z m = ?plus_commutes_rhs_1

5757 plus_commutes (S k) m = ?plus_commutes_rhs_2

5858

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

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

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

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

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

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

102102 plus_commutes Z m = plus_commutes_Z

103103 plus_commutes (S k) m = ?plus_commutes_S

104104

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

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

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

108108

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

334334 plus_commutes_S k Z = Refl

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

336336

337−All metavariables have now been solved.

337+All holes have now been solved.

338338

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

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

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

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

7474===================================

7575

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

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

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

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

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

8080

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

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

7878 The new code is returned with no highlighting.

7979

8080 ``(: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.

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

8383

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

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

8686

8787 ``(: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.

8989

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

9191 Get a list of callers of ``NAME``

docs/reference/repl.rst+2−2

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

104104+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

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

106106+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

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

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

108108+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

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

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

110110+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

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

112112+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

docs/reference/tactics.rst+6−6

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

22Tactics and Theorem Proving

33***************************

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

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

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

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

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.

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

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

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

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

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

10+it to the current module.

1111

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

1313

docs/tutorial/interactive.rst+6−6

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

1616The Idris REPL provides several commands for inspecting and

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

1818splitting 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

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

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

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

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

151151------------

152152

153153The ``: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,

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

156156the 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

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

159159

160160.. code-block:: idris

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

237237

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

239239

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

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

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

242242

243243- ``\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``).

245245

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

247247

248248- ``\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

250250 and the expected type.

251251

252252- ``\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

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

8282

8383When 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

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

8686generated from the module and function names:

8787

8888.. code-block:: idris

8989

9090 *views> :m

91− Global metavariables:

91+ Global holes:

9292 [views.parity_lemma_2,views.parity_lemma_1]

9393

9494The first of these has the following type: