git.iko.soy/Idris-dev
on master help sign in
Document interactive theorem proving as deprecated.

Puts "DEPRECATED:" in the chapter title and also adds a warning paragraph at the start of the tutorial chapter.

commit156fb5ac294838d62dfef0bbad6bd187ba116a63 authorJeremy W. Sherman <jeremyw.sherman@gmail.com> dateWed 12 Aug 2015, 17:47 (11 years ago) parent65f4945
1 file changed+9−3
compare with master
unifiedsplit
docs/proofs/interactive.rst+9−3
docs/proofs/interactive.rst+9−3
@@ -1,6 +1,12 @@
1−***************************
2−Interactive Theorem Proving
3−***************************
1+***************************************
2+DEPRECATED: Interactive Theorem Proving
3+***************************************
4+
5+.. 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.
410
511Idris also supports interactive theorem proving via tactics. This
612is generally not recommended to be used directly, but rather used as a