small correction
commit5379401e0f631811098d0d777800cff06ec425a3
authorMartin Baker <git87465@martinb.com>
dateThu 18 Apr 2019, 08:04 (8 years ago)
parenta38dc57
docs/proofs/interactive.rst+2−1
@@ -23,9 +23,10 @@ rewriteWith and others.
2323``pruviloj`` defines some more advanced derived commands such as:
2424reflexivity and others.
2525
26−To use ``pruviloj`` then call Idris with the "-p pruviloj" option and add:
26+To use ``pruviloj`` call Idris with the "-p pruviloj" option and add:
2727
2828.. code-block:: idris
29+
2930 import Pruviloj
3031 import Pruviloj.Induction
3132