git.iko.soy/Idris-dev
on master help sign in
more small changes
d85b8c6Martin Baker
docs/proofs/example1.rst+8−8
compare with master
unifiedsplit
@@ -83,17 +83,17 @@ The following is a walkthough looking at the state after each tactic:
83 * - Introduce a lambda binding around the current hole and focus on the body.
83 * - Introduce a lambda binding around the current hole and focus on the body.
84 - intro \`{{x}}
84 - intro \`{{x}}
85
85
86− * - state now looks like this
86+ * - The state now looks like this:
87 - .. image:: ../image/elabProofStateEx1_2.png
87 - .. image:: ../image/elabProofStateEx1_2.png
88 :width: 312px
88 :width: 312px
89 :height: 84px
89 :height: 84px
90
90
91− * - logic now looks like this
91+ * - The logic now looks like this:
92 - .. image:: ../image/elabLogicEx1_2.png
92 - .. image:: ../image/elabLogicEx1_2.png
93 :width: 126px
93 :width: 126px
94 :height: 45px
94 :height: 45px
95
95
96− * - term now looks like this
96+ * - The term now looks like this:
97 - ?{hole_0} ≈ λ x . ? {hole_2} . {hole_2} . {hole_0}
97 - ?{hole_0} ≈ λ x . ? {hole_2} . {hole_2} . {hole_0}
98
98
99 * - getEnv
99 * - getEnv
@@ -131,17 +131,17 @@ The following is a walkthough looking at the state after each tactic:
131 * - Place a term into a hole, unifying its type
131 * - Place a term into a hole, unifying its type
132 - fill (Var \`{{x}})
132 - fill (Var \`{{x}})
133
133
134− * - state now looks like this
134+ * - The state now looks like this:
135 - .. image:: ../image/elabProofStateEx1_3.png
135 - .. image:: ../image/elabProofStateEx1_3.png
136 :width: 312px
136 :width: 312px
137 :height: 124px
137 :height: 124px
138
138
139− * - logic now looks like this
139+ * - The logic now looks like this:
140 - .. image:: ../image/elabLogicEx1_3.png
140 - .. image:: ../image/elabLogicEx1_3.png
141 :width: 131px
141 :width: 131px
142 :height: 45px
142 :height: 45px
143
143
144− * - term
144+ * - The term now looks like this:
145 - ?{hole_0} ≈ λ x . ?{hole_2} ≈ x . {hole_2} . {hole_0}
145 - ?{hole_0} ≈ λ x . ?{hole_2} ≈ x . {hole_2} . {hole_0}
146
146
147 * - getEnv
147 * - getEnv
@@ -189,12 +189,12 @@ The following is a walkthough looking at the state after each tactic:
189 * - Substitute a guess into a hole.
189 * - Substitute a guess into a hole.
190 - solve
190 - solve
191
191
192− * - logic now looks like this
192+ * - The logic now looks like this:
193 - .. image:: ../image/elabLogicEx1_4.png
193 - .. image:: ../image/elabLogicEx1_4.png
194 :width: 131px
194 :width: 131px
195 :height: 14px
195 :height: 14px
196
196
197− * - term
197+ * - The term now looks like this:
198 - ?{hole_0} ≈ λ x . x . {hole_0}
198 - ?{hole_0} ≈ λ x . x . {hole_0}
199
199
200 * - getEnv
200 * - getEnv
docs/proofs/primitive.rst+4−3
@@ -457,7 +457,9 @@ Error Handling
457
457
458 fail : List ErrorReportPart -> Elab a
458 fail : List ErrorReportPart -> Elab a
459
459
460− Return type is given by last term so fail cant be at the the last term, we would expect fail to be in some sort of conditional statement:
460+ Note: we may need to make sure the return type 'a' is sufficiently constrained. If required add an explicit type {a = ()}.
461+
462+ Below is some code which includes 'fail'. This will always fail but we could replace 'True' with some more useful condition.
461
463
462 .. code-block:: idris
464 .. code-block:: idris
463
465
@@ -469,10 +471,9 @@ Error Handling
469 fill (Var `{{x}})
471 fill (Var `{{x}})
470 if True
472 if True
471 then
473 then
472− fail [TextPart "error message"]
474+ fail [TextPart "put error message here"]
473 else
475 else
474 solve
476 solve
475
477
476 idNat : Nat -> Nat
478 idNat : Nat -> Nat
477 idNat = %runElab id1
479 idNat = %runElab id1
478−