@@ -83,17 +83,17 @@ The following is a walkthough looking at the state after each tactic:
8383 * - Introduce a lambda binding around the current hole and focus on the body.
8484 - intro \`{{x}}
8585
86− * - state now looks like this
86+ * - The state now looks like this:
8787 - .. image:: ../image/elabProofStateEx1_2.png
8888 :width: 312px
8989 :height: 84px
9090
91− * - logic now looks like this
91+ * - The logic now looks like this:
9292 - .. image:: ../image/elabLogicEx1_2.png
9393 :width: 126px
9494 :height: 45px
9595
96− * - term now looks like this
96+ * - The term now looks like this:
9797 - ?{hole_0} ≈ λ x . ? {hole_2} . {hole_2} . {hole_0}
9898
9999 * - getEnv
@@ -131,17 +131,17 @@ The following is a walkthough looking at the state after each tactic:
131131 * - Place a term into a hole, unifying its type
132132 - fill (Var \`{{x}})
133133
134− * - state now looks like this
134+ * - The state now looks like this:
135135 - .. image:: ../image/elabProofStateEx1_3.png
136136 :width: 312px
137137 :height: 124px
138138
139− * - logic now looks like this
139+ * - The logic now looks like this:
140140 - .. image:: ../image/elabLogicEx1_3.png
141141 :width: 131px
142142 :height: 45px
143143
144− * - term
144+ * - The term now looks like this:
145145 - ?{hole_0} ≈ λ x . ?{hole_2} ≈ x . {hole_2} . {hole_0}
146146
147147 * - getEnv
@@ -189,12 +189,12 @@ The following is a walkthough looking at the state after each tactic:
189189 * - Substitute a guess into a hole.
190190 - solve
191191
192− * - logic now looks like this
192+ * - The logic now looks like this:
193193 - .. image:: ../image/elabLogicEx1_4.png
194194 :width: 131px
195195 :height: 14px
196196
197− * - term
197+ * - The term now looks like this:
198198 - ?{hole_0} ≈ λ x . x . {hole_0}
199199
200200 * - getEnv