@@ -7,7 +7,9 @@ Before looking at the Elab monad we need to know how to construct terms.
77
88
99Proof State
10−===========
10+-----------
11+
12+The terminology 'Proof State' is used by analogy to proof assistants but, as used here, it's really more of a metaprogramming state.
1113
1214Tactics operate on the proof state. The proof state contains various pieces of information, at this stage, the important ones for us are:
1315
@@ -75,9 +77,9 @@ A user defined name can be constructed like this:
7577 )
7678
7779Quasiquotation
78−==============
80+--------------
7981
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:
8183
8284.. list-table:: Quasiquotation
8385
@@ -150,7 +152,7 @@ quasiquotation summary:
150152+------------+-----------+----------------------------------------------------------+
151153
152154TT
153−==
155+--
154156
155157There 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.
156158So 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:
239241
240242Raw
241243---
244+
242245Raw is similar to TT except it is used before types are known. The types should be resolved by the type checker.
243246
244247.. code-block:: idris
@@ -258,7 +261,7 @@ Raw is similar to TT except it is used before types are known. The types should
258261 RConstant Const |
259262
260263Expression Syntax
261−=================
264+-----------------
262265
263266There 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.
264267
@@ -337,7 +340,7 @@ which introduces another guess.
337340The solve tactic completes the proof
338341
339342Binders
340−=======
343+-------
341344
342345Here we look at each tactic in turn to see how they affect the proof state.
343346