fix markup
commit01b7dbcb1f33dffa4c2efa8ae98534fca4018b68
authormartinbaker <git29f185@martinb.com>
dateSat 6 Jul 2019, 08:57 (7 years ago)
parentb0edb5b
docs/proofs/interactive.rst+1−1
@@ -4,7 +4,7 @@ Interactive Theorem Proving
44
55Idris supports interactive theorem proving via elaborator reflection.
66
7−:ref:'elaborator-reflection' is also used to convert high-level Idris code into
7+:ref:`elaborator-reflection` is also used to convert high-level Idris code into
88the core language and for customising the language. Here we show how to use it
99to interactively construct proofs.
1010