diff options
Diffstat (limited to 'doc/refman/RefMan-sch.tex')
| -rw-r--r-- | doc/refman/RefMan-sch.tex | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex index c80e3ceeb1..e28e4a4437 100644 --- a/doc/refman/RefMan-sch.tex +++ b/doc/refman/RefMan-sch.tex @@ -122,14 +122,26 @@ Check odd_even. The type of {\tt even\_odd} shares the same premises but the conclusion is {\tt (n:nat)(even n)->(Q n)}. -\subsection{Automatic declaration of schemes} +\subsection{Automatic declaration of schemes \comindex{Set Boolean Equality Schemes} +\comindex{Unset Boolean Equality Schemes} \comindex{Set Elimination Schemes} +\comindex{Unset Elimination Schemes} +\comindex{Set Nonrecursive Elimination Schemes} +\comindex{Unset Nonrecursive Elimination Schemes} +\label{set-nonrecursive-elimination-schemes} +} It is possible to deactivate the automatic declaration of the induction principles when defining a new inductive type with the {\tt Unset Elimination Schemes} command. It may be reactivated at any time with {\tt Set Elimination Schemes}. + +The types declared with the keywords {\tt Variant} (see~\ref{Variant}) +and {\tt Record} (see~\ref{Record}) do not have an automatic +declaration of the induction principles. It can be activated with the +command {\tt Set Nonrecursive Elimination Schemes}. It can be +deactivated again with {\tt Unset Nonrecursive Elimination Schemes}. \\ You can also activate the automatic declaration of those boolean equalities |