git.iko.soy/Idris-dev
on master help sign in
Point readers at Elaborator Reflection
90b7d07Jeremy W. Sherman
docs/proofs/interactive.rst+2−4
compare with master
unifiedsplit
@@ -3,10 +3,8 @@ DEPRECATED: Interactive Theorem Proving
3***************************************
3***************************************
4
4
5.. warning::
5.. warning::
6− **Interactive theorem-proving has been deprecated.**
6+ The interactive theorem-proving interface documented here has been
7− Support for tactic-based theorem proving will eventually be removed from
7+ deprecated in favor of :ref:`elaborator-reflection`.
8− Idris.
9− Existing tactic-based proofs should be rewritten to use ``rewrite`` instead.
10
8
11Idris also supports interactive theorem proving via tactics. This
9Idris also supports interactive theorem proving via tactics. This
12is generally not recommended to be used directly, but rather used as a
10is generally not recommended to be used directly, but rather used as a
docs/reference/elaborator-reflection.rst+2
@@ -1,3 +1,5 @@
1+.. _elaborator-reflection:
2+
1*********************
3*********************
2Elaborator Reflection
4Elaborator Reflection
3*********************
5*********************