Merge pull request #4718 from martinbaker/interactiveDocFix
fix formatting error which caused missing code block
commit99ac2025ca7ced051e0457729270bf3e386e14b7
authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com>
dateWed 29 May 2019, 12:28 (7 years ago)
parentaed33b80ccc003
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