diff options
Diffstat (limited to 'doc/RecTutorial/RecTutorial.tex')
| -rw-r--r-- | doc/RecTutorial/RecTutorial.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/RecTutorial/RecTutorial.tex b/doc/RecTutorial/RecTutorial.tex index 857ba84d7..0d727e170 100644 --- a/doc/RecTutorial/RecTutorial.tex +++ b/doc/RecTutorial/RecTutorial.tex @@ -2689,7 +2689,7 @@ then appear as subgoals that remain to be solved. In the previous proof, the tactic call ``~\citecoq{apply nat\_ind with (P:= fun n {\funarrow} n {\coqdiff} S n)}~'' can simply be replaced with ``~\citecoq{elim n}~''. The option ``~\citecoq{\texttt{elim} $t$ \texttt{using} $C$}~'' - allows to use a + allows the use of a derived combinator $C$ instead of the default one. Consider the following theorem, stating that equality is decidable on natural numbers: |