From 1638e4bccde4b6922d8a59de92178a5be66406cb Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 7 Jun 2017 19:03:36 +0200 Subject: Fix documentation of Typeclasses eauto := --- doc/refman/Classes.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/refman') diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index acfc4bea93..5966ac468c 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -554,7 +554,7 @@ more efficient resolution behavior (the option is off by default). When a solution to the typeclass goal of this class is found, we never backtrack on it, assuming that it is canonical. -\subsection{\tt Typeclasses eauto := [debug] [dfs | bfs] [\emph{depth}]} +\subsection{\tt Typeclasses eauto := [debug] [(dfs) | (bfs)] [\emph{depth}]} \comindex{Typeclasses eauto} \label{TypeclassesEauto} -- cgit v1.2.3 From 39f36789b986779d36acd36cfa1425487bad43c3 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 12 Jun 2017 12:27:18 +0200 Subject: Document evar naming syntax. --- doc/refman/RefMan-ext.tex | 5 +++++ doc/refman/RefMan-ltac.tex | 2 +- 2 files changed, 6 insertions(+), 1 deletion(-) (limited to 'doc/refman') diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index b475a5233c..3f2dd73a39 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1990,6 +1990,11 @@ Check (fun x y => _) 0 1. Unset Printing Existential Instances. \end{coq_eval} +Existential variables can be named by the user upon creation using +the syntax {\tt ?[\ident]}. This is useful when the existential +variable needs to be explicitly handled later in the script (e.g. +with a named-goal selector, see~\ref{ltac:selector}). + \subsection{Explicit displaying of existential instances for pretty-printing \label{SetPrintingExistentialInstances} \optindex{Printing Existential Instances}} diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 9378529cbe..9caea8f39b 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -392,7 +392,7 @@ all selected goals. \item{} [{\ident}] {\tt :} {\tacexpr} In this variant, {\tacexpr} is applied locally to a goal - previously named by the user. + previously named by the user (see~\ref{ExistentialVariables}). \item {\num} {\tt :} {\tacexpr} -- cgit v1.2.3 From 5cc502fe1b60f59815dfa2819e169dc7ae9b4c7e Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 12 Jun 2017 12:16:34 +0200 Subject: Document Show ident. --- doc/refman/RefMan-pro.tex | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'doc/refman') diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 4c333379bd..9c211b00f3 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -434,6 +434,24 @@ This command displays the current goals. \item \errindex{No focused proof} \end{ErrMsgs} +\item {\tt Show {\ident}.}\\ + Displays the named goal {\ident}. + This is useful in particular to display a shelved goal but only works + if the corresponding existential variable has been named by the user + (see~\ref{ExistentialVariables}) as in the following example. + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\begin{coq_example*} +Goal exists n, n = 0. + eexists ?[n]. +\end{coq_example*} +\begin{coq_example} + Show n. +\end{coq_example} + \item {\tt Show Script.}\comindex{Show Script}\\ Displays the whole list of tactics applied from the beginning of the current proof. -- cgit v1.2.3 From 5636fc49828f6007a8b756cd0517280a73147da6 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 12 Jun 2017 13:04:01 +0200 Subject: Document instantiate (ident := term) and make it the preferred variant. --- doc/refman/RefMan-tac.tex | 24 +++++++++++++++++------- 1 file changed, 17 insertions(+), 7 deletions(-) (limited to 'doc/refman') diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 3f12411863..9707a6c72c 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1429,23 +1429,33 @@ The {\tt evar} tactic creates a new local definition named \ident\ with type \term\ in the context. The body of this binding is a fresh existential variable. -\subsection{\tt instantiate ( {\num} := {\term} )} +\subsection{\tt instantiate ( {\ident} := {\term} )} \tacindex{instantiate} \label{instantiate} The {\tt instantiate} tactic refines (see Section~\ref{refine}) -an existential variable -with the term \term. The \num\ argument is the position of the -existential variable from right to left in the conclusion. This cannot be -the number of the existential variable since this number is different -in every session. +an existential variable {\ident} with the term {\term}. +It is equivalent to {\tt only [\ident]: refine \term} (preferred alternative). -When you are referring to hypotheses which you did not name +\begin{Remarks} +\item To be able to refer to an existential variable by name, the +user must have given the name explicitly (see~\ref{ExistentialVariables}). + +\item When you are referring to hypotheses which you did not name explicitly, be aware that Coq may make a different decision on how to name the variable in the current goal and in the context of the existential variable. This can lead to surprising behaviors. +\end{Remarks} \begin{Variants} + + \item {\tt instantiate ( {\num} := {\term} )} + This variant allows to refer to an existential variable which was not + named by the user. The {\num} argument is the position of the + existential variable from right to left in the goal. + Because this variant is not robust to slight changes in the goal, + its use is strongly discouraged. + \item {\tt instantiate ( {\num} := {\term} ) in \ident} \item {\tt instantiate ( {\num} := {\term} ) in ( Value of {\ident} )} -- cgit v1.2.3 From d4ecb8269b695a972c3e873f08be497b9257d146 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 7 Jun 2017 17:41:53 +0200 Subject: Refactor documentation of records. This fixes bug https://coq.inria.fr/bugs/show_bug.cgi?id=4971 --- doc/refman/RefMan-ext.tex | 255 +++++++++++++++++++++------------------------- 1 file changed, 114 insertions(+), 141 deletions(-) (limited to 'doc/refman') diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index b475a5233c..b118870649 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -29,8 +29,8 @@ construction allows defining ``signatures''. {\recordkw} & ::= & {\tt Record} $|$ {\tt Inductive} $|$ {\tt CoInductive}\\ & & \\ -{\field} & ::= & {\name} \zeroone{\binders} : {\type} [ {\tt where} {\it notation} ] \\ - & $|$ & {\name} \zeroone{\binders} {\typecstr} := {\term} +{\field} & ::= & {\name} \zeroone{\binders} : {\type} \zeroone{{\tt where} {\it notation}} \\ + & $|$ & {\name} \zeroone{\binders} {\typecstrtype} := {\term}\\ \end{tabular} \end{centerframe} \caption{Syntax for the definition of {\tt Record}} @@ -38,21 +38,19 @@ construction allows defining ``signatures''. \end{figure} \noindent In the expression - -\smallskip -{\tt Record} {\ident} {\params} \texttt{:} - {\sort} := {\ident$_0$} \verb+{+ - {\ident$_1$} \binders$_1$ \texttt{:} {\term$_1$}; - \dots - {\ident$_n$} \binders$_n$ \texttt{:} {\term$_n$} \verb+}+. -\smallskip - +\begin{quote} +{\tt Record {\ident} {\params} : {\sort} := {\ident$_0$} \{ \\ + {\ident$_1$} \binders$_1$ : {\term$_1$} ; ... ; \\ + {\ident$_n$} \binders$_n$ : {\term$_n$} \}.} +\end{quote} \noindent the identifier {\ident} is the name of the defined record and {\sort} is its type. The identifier {\ident$_0$} is the name of its constructor. If {\ident$_0$} is omitted, the default name {\tt -Build\_{\ident}} is used. If {\sort} is omitted, the default sort is ``{\Type}''. -The identifiers {\ident$_1$}, .., -{\ident$_n$} are the names of fields and {\tt forall} \binders$_1${\tt ,} {\term$_1$}, ..., {\tt forall} \binders$_n${\tt ,} {\term$_n$} +Build\_{\ident}} is used. +If {\sort} is omitted, the default sort is {\Type}. +The identifiers {\ident$_1$}, \dots, {\ident$_n$} are the names of +fields and {\tt forall {\binders$_1$}, {\term$_1$}}, \dots, +{\tt forall {\binders$_n$}, {\term$_n$}} their respective types. Remark that the type of {\ident$_i$} may depend on the previous {\ident$_j$} (for $j x = 1}. \end{coq_example} -Remark here that the field -\verb+Rat_cond+ depends on the field \verb+bottom+. - -%Let us now see the work done by the {\tt Record} macro. -%First the macro generates an inductive definition -%with just one constructor: -% -%\medskip -%\noindent -%{\tt Inductive {\ident} \zeroone{\binders} : {\sort} := \\ -%\mbox{}\hspace{0.4cm} {\ident$_0$} : forall ({\ident$_1$}:{\term$_1$}) .. -%({\ident$_n$}:{\term$_n$}), {\ident} {\rm\sl params}.} -%\medskip +Remark here that the field \verb+Rat_bottom_cond+ depends +on the field \verb+bottom+ and \verb+Rat_irred_cond+ depends +on both \verb+top+ and \verb+bottom+. Let us now see the work done by the {\tt Record} macro. First the macro generates a variant type definition with just one constructor: \begin{quote} -{\tt Variant {\ident} {\params} :{\sort} :=} \\ -\qquad {\tt - {\ident$_0$} ({\ident$_1$}:{\term$_1$}) .. ({\ident$_n$}:{\term$_n$}).} +{\tt Variant {\ident} {\params} : {\sort} := \\ + {\ident$_0$} ({\ident$_1$} : {\term$_1$}) ... ({\ident$_n$} : {\term$_n$}).} \end{quote} To build an object of type {\ident}, one should provide the constructor {\ident$_0$} with $n$ terms filling the fields of @@ -109,28 +96,9 @@ the record. As an example, let us define the rational $1/2$: \begin{coq_example*} -Require Import Arith. Theorem one_two_irred : forall x y z:nat, x * y = 1 /\ x * z = 2 -> x = 1. -\end{coq_example*} -\begin{coq_eval} -Lemma mult_m_n_eq_m_1 : forall m n:nat, m * n = 1 -> m = 1. -destruct m; trivial. -intros; apply f_equal with (f := S). -destruct m; trivial. -destruct n; simpl in H. - rewrite <- mult_n_O in H. - discriminate. - rewrite <- plus_n_Sm in H. - discriminate. -Qed. - -intros x y z [H1 H2]. - apply mult_m_n_eq_m_1 with (n := y); trivial. -\end{coq_eval} -\ldots -\begin{coq_example*} -Qed. +Admitted. \end{coq_example*} \begin{coq_example} Definition half := mkRat true 1 2 (O_S 1) one_two_irred. @@ -139,33 +107,119 @@ Definition half := mkRat true 1 2 (O_S 1) one_two_irred. Check half. \end{coq_example} +Alternatively, the following syntax allows creating objects by using named fields. The +fields do not have to be in any particular order, nor do they have to be all +present if the missing ones can be inferred or prompted for (see +Section~\ref{Program}). + +\begin{coq_example} +Definition half' := + {| sign := true; + Rat_bottom_cond := O_S 1; + Rat_irred_cond := one_two_irred |}. +\end{coq_example} + +This syntax can be disabled globally for printing by +\begin{quote} +{\tt Unset Printing Records.} +\optindex{Printing Records} +\end{quote} +For a given type, one can override this using either +\begin{quote} +{\tt Add Printing Record {\ident}.} +\end{quote} +to get record syntax or +\begin{quote} +{\tt Add Printing Constructor {\ident}.} +\end{quote} +to get constructor syntax. + +This syntax can also be used for pattern matching. + +\begin{coq_example} +Eval compute in ( + match half with + | {| sign := true; top := n |} => n + | _ => 0 + end). +\end{coq_example} + The macro generates also, when it is possible, the projection functions for destructuring an object of type {\ident}. These -projection functions have the same name that the corresponding +projection functions are given the names of the corresponding fields. If a field is named ``\verb=_='' then no projection is built -for it. In our example: +for it. In our example: + +\begin{coq_example} +Eval compute in top half. +Eval compute in bottom half. +Eval compute in Rat_bottom_cond half. +\end{coq_example} + +An alternative syntax for projections based on a dot notation is +available: \begin{coq_example} Eval compute in half.(top). -Eval compute in half.(bottom). -Eval compute in half.(Rat_bottom_cond). \end{coq_example} + +It can be activated for printing with the command +\optindex{Printing Projections} +\begin{quote} +{\tt Set Printing Projections.} +\end{quote} + +\begin{coq_example} +Set Printing Projections. +Check top half. +\end{coq_example} + +The corresponding grammar rules are given in Figure~\ref{fig:projsyntax}. +When {\qualid} denotes a projection, the syntax {\tt + {\term}.({\qualid})} is equivalent to {\qualid~\term}, the syntax +{\term}{\tt .(}{\qualid}~{\termarg}$_1$ {\ldots} {\termarg}$_n${\tt )} to +{\qualid~{\termarg}$_1$ {\ldots} {\termarg}$_n$~\term}, and the syntax +{\term}{\tt .(@}{\qualid}~{\term}$_1$~\ldots~{\term}$_n${\tt )} to +{@\qualid~{\term}$_1$ {\ldots} {\term}$_n$~\term}. In each case, {\term} +is the object projected and the other arguments are the parameters of +the inductive type. + +\begin{figure}[t] +\begin{centerframe} +\begin{tabular}{lcl} +{\term} & ++= & {\term} {\tt .(} {\qualid} {\tt )}\\ + & $|$ & {\term} {\tt .(} {\qualid} \nelist{\termarg}{} {\tt )}\\ + & $|$ & {\term} {\tt .(} {@}{\qualid} \nelist{\term}{} {\tt )} +\end{tabular} +\end{centerframe} +\caption{Syntax for \texttt{Record} projections} +\label{fig:projsyntax} +\end{figure} + \begin{coq_eval} Reset Initial. \end{coq_eval} -Records defined with the {\tt Record} keyword are not allowed to be -recursive (references to the record's name in the type of its field -raises an error). To define recursive records, one can use the {\tt - Inductive} and {\tt CoInductive} keywords, resulting in an inductive -or co-inductive record. A \emph{caveat}, however, is that records +\begin{Remarks} + +\item Records defined with the {\tt Record} keyword are not allowed to be +recursive (references to the record's name in the type of its field +raises an error). To define recursive records, one can use the {\tt +Inductive} and {\tt CoInductive} keywords, resulting in an inductive +or co-inductive record. +A \emph{caveat}, however, is that records cannot appear in mutually inductive (or co-inductive) definitions. -Induction schemes are automatically generated for inductive records. + +\item Induction schemes are automatically generated for inductive records. Automatic generation of induction schemes for non-recursive records defined with the {\tt Record} keyword can be activated with the {\tt Nonrecursive Elimination Schemes} option (see~\ref{set-nonrecursive-elimination-schemes}). +\item {\tt Structure} is a synonym of the keyword {\tt Record}. + +\end{Remarks} + \begin{Warnings} \item {\tt {\ident$_i$} cannot be defined.} @@ -203,87 +257,6 @@ defined with the {\tt Record} keyword can be activated with the \SeeAlso Coercions and records in Section~\ref{Coercions-and-records} of the chapter devoted to coercions. -\Rem {\tt Structure} is a synonym of the keyword {\tt Record}. - -\Rem Creation of an object of record type can be done by calling {\ident$_0$} -and passing arguments in the correct order. - -\begin{coq_example} -Record point := { x : nat; y : nat }. -Definition a := Build_point 5 3. -\end{coq_example} - -The following syntax allows creating objects by using named fields. The -fields do not have to be in any particular order, nor do they have to be all -present if the missing ones can be inferred or prompted for (see -Section~\ref{Program}). - -\begin{coq_example} -Definition b := {| x := 5; y := 3 |}. -Definition c := {| y := 3; x := 5 |}. -\end{coq_example} - -This syntax can be disabled globally for printing by -\begin{quote} -{\tt Unset Printing Records.} -\optindex{Printing Records} -\end{quote} -For a given type, one can override this using either -\begin{quote} -{\tt Add Printing Record {\ident}.} -\end{quote} -to get record syntax or -\begin{quote} -{\tt Add Printing Constructor {\ident}.} -\end{quote} -to get constructor syntax. - -This syntax can also be used for pattern matching. - -\begin{coq_example} -Eval compute in ( - match b with - | {| y := S n |} => n - | _ => 0 - end). -\end{coq_example} - -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -\Rem An experimental syntax for projections based on a dot notation is -available. The command to activate it is -\optindex{Printing Projections} -\begin{quote} -{\tt Set Printing Projections.} -\end{quote} - -\begin{figure}[t] -\begin{centerframe} -\begin{tabular}{lcl} -{\term} & ++= & {\term} {\tt .(} {\qualid} {\tt )}\\ - & $|$ & {\term} {\tt .(} {\qualid} \nelist{\termarg}{} {\tt )}\\ - & $|$ & {\term} {\tt .(} {@}{\qualid} \nelist{\term}{} {\tt )} -\end{tabular} -\end{centerframe} -\caption{Syntax of \texttt{Record} projections} -\label{fig:projsyntax} -\end{figure} - -The corresponding grammar rules are given Figure~\ref{fig:projsyntax}. -When {\qualid} denotes a projection, the syntax {\tt - {\term}.({\qualid})} is equivalent to {\qualid~\term}, the syntax -{\term}{\tt .(}{\qualid}~{\termarg}$_1$ {\ldots} {\termarg}$_n${\tt )} to -{\qualid~{\termarg}$_1$ {\ldots} {\termarg}$_n$~\term}, and the syntax -{\term}{\tt .(@}{\qualid}~{\term}$_1$~\ldots~{\term}$_n${\tt )} to -{@\qualid~{\term}$_1$ {\ldots} {\term}$_n$~\term}. In each case, {\term} -is the object projected and the other arguments are the parameters of -the inductive type. - -To deactivate the printing of projections, use -{\tt Unset Printing Projections}. - \subsection{Primitive Projections} \optindex{Primitive Projections} \optindex{Printing Primitive Projection Parameters} -- cgit v1.2.3 From 0577523398277863ef7fbdbc37a8d19e26ba6b6f Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Fri, 23 Jun 2017 10:24:31 -0400 Subject: Fix Bug #5574, document function scope --- doc/refman/RefMan-ltac.tex | 2 +- doc/refman/RefMan-syn.tex | 72 +++++++++++++++++++++++++++++----------------- 2 files changed, 46 insertions(+), 28 deletions(-) (limited to 'doc/refman') diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 9378529cbe..acff7816c8 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -873,7 +873,7 @@ behavior can be retrieved with the {\tt Tactic Compat Context} flag. \end{Variants} -\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}} +\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}}\label{ltac-match-goal} \index{Ltac!match reverse goal@\texttt{match reverse goal}} \index{match goal@\texttt{match goal}!in Ltac} \index{match reverse goal@\texttt{match reverse goal}!in Ltac}} diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index 21c39de967..edcf0fcf4b 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -883,7 +883,8 @@ statically. For instance, if {\tt f} is a polymorphic function of type recognized as an argument to be interpreted in scope {\scope}. \comindex{Bind Scope} -More generally, any {\class} (see Chapter~\ref{Coercions-full}) can be +\label{bindscope} +More generally, any coercion {\class} (see Chapter~\ref{Coercions-full}) can be bound to an interpretation scope. The command to do it is \begin{quote} {\tt Bind Scope} {\scope} \texttt{with} {\class} @@ -902,7 +903,7 @@ Open Scope nat_scope. (* Define + on the nat as the default for + *) Check (fun x y1 y2 z t => P _ (x + t) ((f _ (y1 + y2) + z))). \end{coq_example} -\Rem The scope {\tt type\_scope} has also a local effect on +\Rem The scopes {\tt type\_scope} and {\tt function\_scope} also have a local effect on interpretation. See the next section. \SeeAlso The command to show the scopes bound to the arguments of a @@ -912,10 +913,21 @@ function is described in Section~\ref{About}. The scope {\tt type\_scope} has a special status. It is a primitive interpretation scope which is temporarily activated each time a -subterm of an expression is expected to be a type. This includes goals -and statements, types of binders, domain and codomain of implication, -codomain of products, and more generally any type argument of a -declared or defined constant. +subterm of an expression is expected to be a type. It is delimited by +the key {\tt type}, and bound to the coercion class {\tt Sortclass}. It is also +used in certain situations where an expression is statically known to +be a type, including the conclusion and the type of hypotheses within +an {\tt Ltac} goal match (see Section~\ref{ltac-match-goal}) +the statement of a theorem, the type of +a definition, the type of a binder, the domain and codomain of +implication, the codomain of products, and more generally any type +argument of a declared or defined constant. + +\subsection[The {\tt function\_scope} interpretation scope]{The {\tt function\_scope} interpretation scope\index{function\_scope@\texttt{function\_scope}}} + +The scope {\tt function\_scope} also has a special status. +It is temporarily activated each time the argument of a global reference is +recognized to be a {\tt Funclass instance}, i.e., of type {\tt forall x:A, B} or {\tt A -> B}. \subsection{Interpretation scopes used in the standard library of {\Coq}} @@ -925,38 +937,39 @@ commands {\tt Print Scopes} or {\tt Print Scope {\scope}}. \subsubsection{\tt type\_scope} -This includes infix {\tt *} for product types and infix {\tt +} for -sum types. It is delimited by key {\tt type}. +This scope includes infix {\tt *} for product types and infix {\tt +} for +sum types. It is delimited by key {\tt type}, and bound to the coercion class +{\tt Sortclass}, as described at \ref{bindscope}. \subsubsection{\tt nat\_scope} -This includes the standard arithmetical operators and relations on +This scope includes the standard arithmetical operators and relations on type {\tt nat}. Positive numerals in this scope are mapped to their canonical representent built from {\tt O} and {\tt S}. The scope is -delimited by key {\tt nat}. +delimited by key {\tt nat}, and bound to the type {\tt nat} (see \ref{bindscope}). \subsubsection{\tt N\_scope} -This includes the standard arithmetical operators and relations on +This scope includes the standard arithmetical operators and relations on type {\tt N} (binary natural numbers). It is delimited by key {\tt N} and comes with an interpretation for numerals as closed term of type {\tt Z}. \subsubsection{\tt Z\_scope} -This includes the standard arithmetical operators and relations on +This scope includes the standard arithmetical operators and relations on type {\tt Z} (binary integer numbers). It is delimited by key {\tt Z} and comes with an interpretation for numerals as closed term of type {\tt Z}. \subsubsection{\tt positive\_scope} -This includes the standard arithmetical operators and relations on +This scope includes the standard arithmetical operators and relations on type {\tt positive} (binary strictly positive numbers). It is delimited by key {\tt positive} and comes with an interpretation for numerals as closed term of type {\tt positive}. \subsubsection{\tt Q\_scope} -This includes the standard arithmetical operators and relations on +This scope includes the standard arithmetical operators and relations on type {\tt Q} (rational numbers defined as fractions of an integer and a strictly positive integer modulo the equality of the numerator-denominator cross-product). As for numerals, only $0$ and @@ -965,13 +978,13 @@ interpretations are $\frac{0}{1}$ and $\frac{1}{1}$ respectively). \subsubsection{\tt Qc\_scope} -This includes the standard arithmetical operators and relations on the +This scope includes the standard arithmetical operators and relations on the type {\tt Qc} of rational numbers defined as the type of irreducible fractions of an integer and a strictly positive integer. \subsubsection{\tt real\_scope} -This includes the standard arithmetical operators and relations on +This scope includes the standard arithmetical operators and relations on type {\tt R} (axiomatic real numbers). It is delimited by key {\tt R} and comes with an interpretation for numerals as term of type {\tt R}. The interpretation is based on the binary decomposition. The @@ -986,35 +999,40 @@ those of {\tt R}. \subsubsection{\tt bool\_scope} -This includes notations for the boolean operators. It is -delimited by key {\tt bool}. +This scope includes notations for the boolean operators. It is +delimited by key {\tt bool}, and bound to the type {\tt bool} (see \ref{bindscope}). \subsubsection{\tt list\_scope} -This includes notations for the list operators. It is -delimited by key {\tt list}. +This scope includes notations for the list operators. It is +delimited by key {\tt list}, and bound to the type {\tt list} (see \ref{bindscope}). + +\subsubsection{\tt function\_scope} + +This scope is delimited by the key {\tt function}, and bound to the coercion class {\tt Funclass}, +as described at \ref{bindscope}. \subsubsection{\tt core\_scope} -This includes the notation for pairs. It is delimited by key {\tt core}. +This scope includes the notation for pairs. It is delimited by key {\tt core}. \subsubsection{\tt string\_scope} -This includes notation for strings as elements of the type {\tt +This scope includes notation for strings as elements of the type {\tt string}. Special characters and escaping follow {\Coq} conventions on strings (see Section~\ref{strings}). Especially, there is no convention to visualize non printable characters of a string. The file {\tt String.v} shows an example that contains quotes, a newline -and a beep (i.e. the ascii character of code 7). +and a beep (i.e. the ASCII character of code 7). \subsubsection{\tt char\_scope} -This includes interpretation for all strings of the form -\verb!"!$c$\verb!"! where $c$ is an ascii character, or of the form +This scope includes interpretation for all strings of the form +\verb!"!$c$\verb!"! where $c$ is an ASCII character, or of the form \verb!"!$nnn$\verb!"! where $nnn$ is a three-digits number (possibly with leading 0's), or of the form \verb!""""!. Their respective -denotations are the ascii code of $c$, the decimal ascii code $nnn$, -or the ascii code of the character \verb!"! (i.e. the ascii code +denotations are the ASCII code of $c$, the decimal ASCII code $nnn$, +or the ASCII code of the character \verb!"! (i.e. the ASCII code 34), all of them being represented in the type {\tt ascii}. \subsection{Displaying informations about scopes} -- cgit v1.2.3