diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-08 16:50:17 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-08 16:50:17 +0000 |
commit | 09580d08476cfa3f50b8c9a347293525c9f022fc (patch) | |
tree | 0968ee37bdac87ac4a3efac14f4f518c1121ed43 /doc/refman/Program.tex | |
parent | c164dc2aadd8d26b362669b9af6b45cbd8e563ff (diff) |
New "Preterm [ of id ] " command to show the preterm before giving it to
Coq (solves part 2 of bug #1784). Add corresponding documentation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10530 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman/Program.tex')
-rw-r--r-- | doc/refman/Program.tex | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index 0d9422dd9..6e3cb4c4b 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -222,6 +222,8 @@ tactic is replaced by the default one if not specified. one (useful for mutually recursive definitions). \item {\tt Admit Obligations [of \ident]} Admits all obligations (does not work with structurally recursive programs). +\item {\tt Preterm [of \ident]} Shows the term that will be fed to + the kernel once the obligations are solved. Useful for debugging. \end{itemize} The module {\tt Coq.Program.Tactics} defines the default tactic for solving @@ -254,10 +256,11 @@ Program Fixpoint f (x : A | P) { measure size } := You will then just have to prove that the measure decreases at each recursive call. There are three drawbacks though: \begin{enumerate} - \item You have to define size yourself; + \item You have to define the measure yourself; \item The reduction is a little more involved, although it works using lazy evaluation; - \item Mutual recursion isn't possible anymore. What would it mean ? + \item Mutual recursion on the underlying inductive type isn't possible + anymore, but nested mutual recursion is always possible. \end{enumerate} \end{itemize} |