diff options
Diffstat (limited to 'doc/refman/RefMan-tacex.tex')
-rw-r--r-- | doc/refman/RefMan-tacex.tex | 27 |
1 files changed, 18 insertions, 9 deletions
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex index 57155d21..0aee4317 100644 --- a/doc/refman/RefMan-tacex.tex +++ b/doc/refman/RefMan-tacex.tex @@ -373,10 +373,11 @@ with forest : Set := \end{coq_example*} We define the function \texttt{tree\_size} that computes the size -of a tree or a forest. +of a tree or a forest. Note that we use \texttt{Function} which +generally produces better principles. \begin{coq_example*} -Fixpoint tree_size (t:tree) : nat := +Function tree_size (t:tree) : nat := match t with | node A f => S (forest_size f) end @@ -387,23 +388,31 @@ Fixpoint tree_size (t:tree) : nat := end. \end{coq_example*} -The definition of principle of mutual induction following the -recursive structure of \texttt{tree\_size} is defined by the -command: +Remark: \texttt{Function} generates itself non mutual induction +principles {\tt tree\_size\_ind} and {\tt forest\_size\_ind}: + +\begin{coq_example} +Check tree_size_ind. +\end{coq_example} + +The definition of mutual induction principles following the recursive +structure of \texttt{tree\_size} and \texttt{forest\_size} is defined +by the command: \begin{coq_example*} -Functional Scheme tree_size_ind := Induction for tree_size Sort Prop -with forest_size_ind := Induction for forest_size Sort Prop. +Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop +with forest_size_ind2 := Induction for forest_size Sort Prop. \end{coq_example*} -You may now look at the type of {\tt tree\_size\_ind}: +You may now look at the type of {\tt tree\_size\_ind2}: \begin{coq_example} -Check tree_size_ind. +Check tree_size_ind2. \end{coq_example} + \section{{\tt inversion}} \tacindex{inversion} \label{inversion-examples} |