diff options
Diffstat (limited to 'doc/refman/RefMan-ind.tex')
| -rw-r--r-- | doc/refman/RefMan-ind.tex | 24 |
1 files changed, 21 insertions, 3 deletions
diff --git a/doc/refman/RefMan-ind.tex b/doc/refman/RefMan-ind.tex index 3389382af0..52935b93c1 100644 --- a/doc/refman/RefMan-ind.tex +++ b/doc/refman/RefMan-ind.tex @@ -468,9 +468,9 @@ natural in case of inductively defined relations. \Example With the predicates {\tt odd} and {\tt even} inductively defined as: -\begin{coq_eval} -Restore State "Initial". -\end{coq_eval} +% \begin{coq_eval} +% Restore State "Initial". +% \end{coq_eval} \begin{coq_example*} Inductive odd : nat -> Prop := oddS : forall n:nat, even n -> odd (S n) @@ -491,7 +491,25 @@ 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{\tt Combined Scheme ...}\index{CombinedScheme@{\tt Combined Scheme}}\label{CombinedScheme} +\label{combinedscheme} +The {\tt Combined Scheme} command is a tool for combining +induction principles generated by the {\tt Scheme} command. +Its syntax follows the schema : +\noindent +{\tt Combined Scheme {\ident$_0$} from {\ident$_1$}, .., {\ident$_n$}}\\ +\ident$_1$ \ldots \ident$_n$ are different inductive principles that must belong to +the same package of mutual inductive principle definitions. This command +generates {\ident$_0$} to be the conjunction of the principles: it is +build from the common premises of the principles and concluded by the +conjunction of their conclusions. For exemple, we can combine the +induction principles for trees and forests: + +\begin{coq_example*} +Mutual Scheme tree_forest_mutind from tree_ind, forest_ind. +Check tree_forest_mutind. +\end{coq_example*} %\end{document} |