diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /doc/refman/RefMan-gal.tex | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'doc/refman/RefMan-gal.tex')
-rw-r--r-- | doc/refman/RefMan-gal.tex | 21 |
1 files changed, 15 insertions, 6 deletions
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index d1489591..204fa90d 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -217,12 +217,12 @@ possible one (among all tokens defined at this moment), and so on. \subsection{Syntax of terms} -Figures \ref{term-syntax} and \ref{term-syntax-aux} describe the basic -set of terms which form the {\em Calculus of Inductive Constructions} -(also called \CIC). The formal presentation of {\CIC} is given in -Chapter \ref{Cic}. Extensions of this syntax are given in chapter -\ref{Gallina-extension}. How to customize the syntax is described in -Chapter \ref{Addoc-syntax}. +Figures \ref{term-syntax} and \ref{term-syntax-aux} describe the basic syntax of +the terms of the {\em Calculus of Inductive Constructions} (also +called \CIC). The formal presentation of {\CIC} is given in Chapter +\ref{Cic}. Extensions of this syntax are given in chapter +\ref{Gallina-extension}. How to customize the syntax is described in Chapter +\ref{Addoc-syntax}. \begin{figure}[htbp] \begin{centerframe} @@ -240,9 +240,13 @@ Chapter \ref{Addoc-syntax}. & $|$ & {\tt let} {\tt (} \sequence{\name}{,} {\tt )} \zeroone{\ifitem} {\tt :=} {\term} {\tt in} {\term} &(\ref{caseanalysis}, \ref{Mult-match})\\ + & $|$ & {\tt let '} {\pattern} \zeroone{{\tt in} {\term}} {\tt :=} {\term} + \zeroone{\returntype} {\tt in} {\term} & (\ref{caseanalysis}, \ref{Mult-match})\\ & $|$ & {\tt if} {\term} \zeroone{\ifitem} {\tt then} {\term} {\tt else} {\term} &(\ref{caseanalysis}, \ref{Mult-match})\\ & $|$ & {\term} {\tt :} {\term} &(\ref{typecast})\\ + & $|$ & {\term} {\tt <:} {\term} &(\ref{typecast})\\ + & $|$ & {\term} {\tt :>} &(\ref{ProgramSyntax})\\ & $|$ & {\term} {\tt ->} {\term} &(\ref{products})\\ & $|$ & {\term} \nelist{\termarg}{}&(\ref{applications})\\ & $|$ & {\tt @} {\qualid} \sequence{\term}{} @@ -256,6 +260,7 @@ Chapter \ref{Addoc-syntax}. & $|$ & {\sort} &(\ref{Gallina-sorts})\\ & $|$ & {\num} &(\ref{numerals})\\ & $|$ & {\_} &(\ref{hole})\\ + & $|$ & {\tt (} {\term} {\tt )} & \\ & & &\\ {\termarg} & ::= & {\term} &\\ & $|$ & {\tt (} {\ident} {\tt :=} {\term} {\tt )} @@ -496,6 +501,10 @@ arguments is used for making explicit the value of implicit arguments The expression ``{\term}~{\tt :}~{\type}'' is a type cast expression. It enforces the type of {\term} to be {\type}. +``{\term}~{\tt <:}~{\type}'' locally sets up the virtual machine (as if option +{\tt Virtual Machine} were on, see \ref{SetVirtualMachine}) for checking that +{\term} has type {\type}. + \subsection{Inferable subterms \label{hole} \index{\_}} |