git.iko.soy/Idris-dev
on master help sign in
fix markup
01b7dbcmartinbaker
docs/proofs/interactive.rst+1−1
compare with master
unifiedsplit
@@ -4,7 +4,7 @@ Interactive Theorem Proving
4
4
5Idris supports interactive theorem proving via elaborator reflection.
5Idris supports interactive theorem proving via elaborator reflection.
6
6
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
8the core language and for customising the language. Here we show how to use it
8the core language and for customising the language. Here we show how to use it
9to interactively construct proofs.
9to interactively construct proofs.
10
10