diff options
| -rw-r--r-- | Makefile.doc | 2 | ||||
| -rw-r--r-- | doc/refman/Program.tex | 29 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 23 |
3 files changed, 38 insertions, 16 deletions
diff --git a/Makefile.doc b/Makefile.doc index fedde37483..3705c047a2 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -86,7 +86,7 @@ doc/refman/Reference-Manual.dvi: $(DOCCOMMON) $(REFMANFILES) $(LATEX) Reference-Manual;\ $(LATEX) Reference-Manual) -doc/refman/Reference-Manual.pdf: doc/refman/Reference-Manual.tex +doc/refman/Reference-Manual.pdf: $(REFMANFILES) doc/refman/Reference-Manual.tex (cd doc/refman; $(PDFLATEX) Reference-Manual.tex) ### Reference Manual (browsable format) diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index 6e3cb4c4b2..e06e3e70e1 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -133,6 +133,7 @@ The structural fixpoint operator behaves just like the one of Coq It works with mutually recursive definitions too. \begin{coq_example} +Require Import Program. Program Fixpoint div2 (n : nat) : { x : nat | n = 2 * x \/ n = 2 * x + 1 } := match n with | S (S p) => S (div2 p) @@ -150,11 +151,12 @@ You can use a well-founded order or a measure as termination orders using the sy \begin{coq_eval} Reset Initial. Require Import Arith. +Require Import Program. \end{coq_eval} \begin{coq_example} Definition id (n : nat) := n. - -Program Fixpoint div2 (n : nat) {measure id n} : { x : nat | n = 2 * x \/ n = 2 * x + 1 } := +Program Fixpoint div2 (n : nat) {measure id n} : + { x : nat | n = 2 * x \/ n = 2 * x + 1 } := match n with | S (S p) => S (div2 p) | _ => O @@ -206,23 +208,27 @@ obligations (e.g. when defining mutually recursive blocks). The optional tactic is replaced by the default one if not specified. \begin{itemize} -\item {\tt Obligations Tactic := \tacexpr} Sets the default obligation +\item {\tt Obligations Tactic := \tacexpr}\comindex{Obligations Tactic} + Sets the default obligation solving tactic applied to all obligations automatically, whether to solve them or when starting to prove one, e.g. using {\tt Next}. -\item {\tt Obligations [of \ident]} Displays all remaining +\item {\tt Obligations [of \ident]}\comindex{Obligations} Displays all remaining obligations. -\item {\tt Next Obligation [of \ident]} Start the proof of the next - unsolved obligation. -\item {\tt Obligation num [of \ident]} Start the proof of +\item {\tt Obligation num [of \ident]}\comindex{Obligation} Start the proof of obligation {\tt num}. -\item {\tt Solve Obligations [of \ident] [using \tacexpr]} Tries to solve +\item {\tt Next Obligation [of \ident]}\comindex{Next Obligation} Start the proof of the next + unsolved obligation. +\item {\tt Solve Obligations [of \ident] [using + \tacexpr]}\comindex{Solve Obligations} + Tries to solve each obligation of \ident using the given tactic or the default one. \item {\tt Solve All Obligations [using \tacexpr]} Tries to solve each obligation of every program using the given tactic or the default 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 +\item {\tt Admit Obligations [of \ident]}\comindex{Admit Obligations} + Admits all obligations (does not work with structurally recursive programs). +\item {\tt Preterm [of \ident]}\comindex{Preterm} + Shows the term that will be fed to the kernel once the obligations are solved. Useful for debugging. \end{itemize} @@ -231,7 +237,6 @@ obligations called {\tt program\_simpl}. Importing {\tt Coq.Program.Program} also adds some useful notations, as documented in the file itself. \section{Frequently Asked Questions - \comindex{Program FAQ} \label{ProgramFAQ}} \begin{itemize} diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 5dc06f33cc..de6b93b424 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1133,23 +1133,40 @@ a-priori and a-posteriori. In the first setting, one wants to explicitely give the implicit arguments of a constant as part of its definition. To do this, one has -to surround the bindings of implicit arguments by backquotes: +to surround the bindings of implicit arguments by curly braces: \begin{coq_eval} Reset Initial. \end{coq_eval} \begin{coq_example} -Definition id `A : Type` (x : A) : A := x. +Definition id {A : Type} (x : A) : A := x. \end{coq_example} This automatically declares the argument {\tt A} of {\tt id} as a maximally inserted implicit argument. One can then do as-if the argument was absent in every situation but still be able to specify it if needed: \begin{coq_example} -Definition compose `A B C` (g : B -> C) (f : A -> B) := +Definition compose {A B C} (g : B -> C) (f : A -> B) := fun x => g (f x). Goal forall A, compose id id = id (A:=A). \end{coq_example} +The syntax is supported in all top-level definitions: {\tt Definition}, +{\tt Fixpoint}, {\tt Lemma} and so on. For (co-)inductive datatype +declarations, the semantics are the following: an inductive parameter +declared as an implicit argument need not be repeated in the inductive +definition but will become implicit for the constructors of the +inductive only, not the inductive type itself. For example: + +\begin{coq_example} +Inductive list {A : Type} : Type := +| nil : list +| cons : A -> list -> list. +Print list. +\end{coq_example} + +One can always specify the parameter if it is not uniform using the +usual implicit arguments disambiguation syntax. + \subsubsection{The Implicit Arguments Vernacular Command} To set implicit arguments for a constant a-posteriori, one can use the |