@@ -56,7 +56,7 @@ their docstrings:
57.. code-block:: idris
57.. code-block:: idris
59−*plusReducesZ> :doc intro
59+ *plusReducesZ> :doc intro
60 Language.Reflection.Elab.Tactics.intro : (n : TTName) -> Elab ()
60 Language.Reflection.Elab.Tactics.intro : (n : TTName) -> Elab ()
61 Introduce a lambda binding around the current hole and focus on the
61 Introduce a lambda binding around the current hole and focus on the
62 body. Requires that the hole be in binding form (use attack).
62 body. Requires that the hole be in binding form (use attack).
@@ -71,7 +71,7 @@ their docstrings:
72.. code-block:: idris
72.. code-block:: idris
74−*plusReducesZ> :doc rewriteWith
74+ *plusReducesZ> :doc rewriteWith
75 Language.Reflection.Elab.Tactics.rewriteWith : Raw -> Elab ()
75 Language.Reflection.Elab.Tactics.rewriteWith : Raw -> Elab ()
76 Attempt to rewrite the goal using an equality.
76 Attempt to rewrite the goal using an equality.