@@ -1,57 +1,46 @@
1−Example 1
1+Elaborator Reflection - Identity Example
2−=========
2+========================================
4−.. list-table:: Nat identity
4+.. list-table::
6− * - As an example of elaborator reflection here we step through this identity implementation:
6+ * - This example of elaborator reflection steps through this metaprogram that generates the identity function:
9− .. code-block:: idris
7+ - .. code-block:: idris
11 %language ElabReflection
9 %language ElabReflection
13 idNat : Nat -> Nat
11 idNat : Nat -> Nat
14− idNat = %runElab (do
12+ idNat = %runElab (do intro `{{x}}
16− fill (Var `{{x}})
13+ fill (Var `{{x}})
20−.. list-table:: Nat identity
16+.. list-table::
22− * - We start off with a hole for the whole term (of type Nat->Nat).
18+ * - At the beginning of executing the elaboration script, the initial state consists of a single hole of type Nat -> Nat.
23− We fill that with 'intro' which creates a lambda term with a hole for the expression.
20+ Fill that with 'intro' which creates a lambda term with a hole for the expression.
26− .. image:: ../image/tree.png
21+ - .. image:: ../image/tree.png
27 :width: 133px
22 :width: 133px
28 :height: 106px
23 :height: 106px
30−After each tactic we will look at the state:
25+The following is a walkthough looking at the state after each tactic:
32−.. list-table:: evolution of state
27+.. list-table::
34− * - We start with the type signature like this:
29+ * - Start with the type signature like this:
37− .. code-block:: idris
30+ - .. code-block:: idris
39 %language ElabReflection
32 %language ElabReflection
41 idNat : Nat -> Nat
34 idNat : Nat -> Nat
42 idNat = %runElab (do
35 idNat = %runElab (do
44− * - In order to investigate how the program works we can look at the proofState at each stage as the tactics are applied. So here is the proofState at the start:
37+ * - In order to investigate how the program works this table shows the proofState at each stage as the tactics are applied. So here is the proofState at the start:
47− .. image:: ../image/elabProofStateEx1_1.png
38+ - .. image:: ../image/elabProofStateEx1_1.png
48 :width: 310px
39 :width: 310px
49 :height: 124px
40 :height: 124px
51− * - We can also look at the logic at each stage:
42+ * - This table also shows the logic at each stage:
54− .. image:: ../image/elabLogicEx1_1.png
43+ - .. image:: ../image/elabLogicEx1_1.png
55 :width: 126px
44 :width: 126px
56 :height: 33px
45 :height: 33px
@@ -64,9 +53,7 @@ After each tactic we will look at the state:
69− .. code-block:: idris
56+ - .. code-block:: idris