@@ -7,7 +7,9 @@ Before looking at the Elab monad we need to know how to construct terms.
10−===========
10+-----------
12+The terminology 'Proof State' is used by analogy to proof assistants but, as used here, it's really more of a metaprogramming state.
12Tactics operate on the proof state. The proof state contains various pieces of information, at this stage, the important ones for us are:
14Tactics operate on the proof state. The proof state contains various pieces of information, at this stage, the important ones for us are:
@@ -75,9 +77,9 @@ A user defined name can be constructed like this:
77Quasiquotation
79Quasiquotation
78−==============
80+--------------
80−Since names are used frequently in elaborator reflection there is a shortcut for constructing them:
82+Since names are used frequently in elaborator reflection there is a shortcut for constructing them:
82.. list-table:: Quasiquotation
84.. list-table:: Quasiquotation
@@ -150,7 +152,7 @@ quasiquotation summary:
150+------------+-----------+----------------------------------------------------------+
152+------------+-----------+----------------------------------------------------------+
155There is a notation for a term in TT as it is being constructed (based on a BNF-like grammar), this is used for example in the debug output, it is a compact way to see the state of the term so it is used here.
157There is a notation for a term in TT as it is being constructed (based on a BNF-like grammar), this is used for example in the debug output, it is a compact way to see the state of the term so it is used here.
156So internally the program is stored as a tree structure using the following syntax:
158So internally the program is stored as a tree structure using the following syntax:
@@ -239,6 +241,7 @@ De Bruijn index which is a integer where:
242Raw is similar to TT except it is used before types are known. The types should be resolved by the type checker.
245Raw is similar to TT except it is used before types are known. The types should be resolved by the type checker.
244.. code-block:: idris
247.. code-block:: idris
@@ -258,7 +261,7 @@ Raw is similar to TT except it is used before types are known. The types should
258 RConstant Const |
261 RConstant Const |
260Expression Syntax
263Expression Syntax
261−=================
264+-----------------
263There is a way of notating expressions such as those used in the proof state (example: goal type and proof terms) which is reasonably standard in the papers written about this subject.
266There is a way of notating expressions such as those used in the proof state (example: goal type and proof terms) which is reasonably standard in the papers written about this subject.
@@ -337,7 +340,7 @@ which introduces another guess.
337The solve tactic completes the proof
340The solve tactic completes the proof
342Here we look at each tactic in turn to see how they affect the proof state.
345Here we look at each tactic in turn to see how they affect the proof state.