Point readers at Elaborator Reflection
This replaces the previous advice to adopt rewrite-style proofs instead of
the deprecated interactive theorem proving system.
This also un-bolds the deprecation warning body because, for whatever reason,
Sphinx rendered the raw text of the ref:`elaborator-reflection` markup
with the bold markup in place. Removing the bold let the section reference
work as expected. Yay, edge cases!
commit90b7d070a01652cff1774c911fa3ae3029764145
authorJeremy W. Sherman <jeremyw.sherman@gmail.com>
dateSat 15 Aug 2015, 15:57 (11 years ago)
parent156fb5a
docs/proofs/interactive.rst+2−4
@@ -3,10 +3,8 @@ DEPRECATED: Interactive Theorem Proving
33***************************************
44
55.. warning::
6− **Interactive theorem-proving has been deprecated.**
7− Support for tactic-based theorem proving will eventually be removed from
8− Idris.
9− Existing tactic-based proofs should be rewritten to use ``rewrite`` instead.
6+ The interactive theorem-proving interface documented here has been
7+ deprecated in favor of :ref:`elaborator-reflection`.
108
119Idris also supports interactive theorem proving via tactics. This
1210is 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+
13*********************
24Elaborator Reflection
35*********************