git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2518 from jeremy-w/jeremy-w/mark-interactive-proving-as-deprecated

Document interactive theorem proving as deprecated.

commita0d8376256865b53099cc51bc25af6d39329f38e authorNiklas Larsson <metaniklas@gmail.com> dateSun 6 Sep 2015, 19:43 (11 years ago) parent88005d890b7d07
2 files changed+9−3
compare with master
unifiedsplit
docs/proofs/interactive.rst+7−3 docs/reference/elaborator-reflection.rst+2
docs/proofs/interactive.rst+7−3
@@ -1,6 +1,10 @@
1−***************************
2−Interactive Theorem Proving
3−***************************
1+***************************************
2+DEPRECATED: Interactive Theorem Proving
3+***************************************
4+
5+.. warning::
6+ The interactive theorem-proving interface documented here has been
7+ deprecated in favor of :ref:`elaborator-reflection`.
48
59Idris also supports interactive theorem proving via tactics. This
610is 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*********************