diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 70b9be8acc1d1ada178a95c1cd4013506e9d0d1b (patch) | |
tree | f672a286d962cc67c95874b3b60402fc957870b6 /doc/refman/RefMan-tacex.tex | |
parent | a5bd4e097a94cc4f863bf4d4bcc5ce592c30ba47 (diff) | |
parent | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff) |
Merge commit 'upstream/8.1.gamma' into 8.1
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} |