diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-02 23:29:27 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-06 08:36:03 +0100 |
| commit | 9565a7fe6a1a989300e230f14cf748a3b115c217 (patch) | |
| tree | 3d169a66d0a7fa72d55b6ba3b7a9360449c7987a /doc/refman/RefMan-cic.tex | |
| parent | 1dfb2c020fa0ed2e853539b8b398a9d91cbbeefa (diff) | |
RefMan, ch. 4: Terminology constant/names.
Diffstat (limited to 'doc/refman/RefMan-cic.tex')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 15b8fb9c8..a5471ac14 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -140,7 +140,8 @@ identifier with a number) or a successor of an algebraic universe (an expression $u+1$), or an upper bound of algebraic universes (an expression $max(u_1,...,u_n)$), or the base universe (the expression $0$) which corresponds, in the arity of sort-polymorphic inductive -types, to the predicative sort {\Set}. A graph of constraints between +types (see Section \ref{Sort-polymorphism-inductive}), +to the predicative sort {\Set}. A graph of constraints between the universe variables is maintained globally. To ensure the existence of a mapping of the universes to the positive integers, the graph of constraints must remain acyclic. Typing expressions that violate the @@ -148,9 +149,10 @@ acyclicity of the graph of constraints results in a \errindex{Universe inconsistency} error (see also Section~\ref{PrintingUniverses}). \subsection{Constants} -Besides the sorts, the language also contains constants denoting -objects in the environment. These constants may denote previously -defined objects but also objects related to inductive definitions + +Constants refers to +objects in the global environment. These constants may denote previously +defined objects, but also objects related to inductive definitions (either the type itself or one of its constructors or destructors). \medskip\noindent {\bf Remark. } In other presentations of \CIC, @@ -174,7 +176,7 @@ in a theory where inductive objects are represented by terms. \subsection{Terms} -Terms are built from variables, global names, constructors, +Terms are built from variables, constants, constructors, abstraction, application, local declarations bindings (``let-in'' expressions) and product. |