fix formatting error which caused missing code block
commit0ccc003086b3d20eecd58825122518e4096571cc
authorMartin Baker <git87465@martinb.com>
dateFri 24 May 2019, 17:18 (7 years ago)
parented4d4cf
docs/proofs/interactive.rst+1
@@ -153,6 +153,7 @@ This has been normalised to ``0 = 0`` so now we have to prove that ``0`` equals
153153is easy to prove by reflexivity from the pruviloj library:
154154
155155.. code-block:: idris
156+
156157 -Main.plusredZ_Z> reflexivity
157158 plusredZ_Z: No more goals.
158159