diff options
| -rw-r--r-- | CHANGES | 19 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 31 |
2 files changed, 32 insertions, 18 deletions
@@ -15,24 +15,7 @@ Logic Records with primitive projections have eta-conversion, the canonical form being [mkR pars (p1 t) ... (pn t)]. - With native projections, the parsing of projection applications changes: - - - r.(p) and (p r) elaborate to native projection application, and - the parameters cannot be mentioned. The following arguments are - parsed according to the remaining implicit arguments declared for the - projection (i.e. the implicit arguments after the record type - argument). In dot notation, the record type argument is considered - explicit no matter what its implicit status is. - - r.(@p params) and @p args are parsed as regular applications of the - projection with explicit parameters. - - [simpl p] is forbidden, but [simpl @p] will simplify both the projection - and its explicit [@p] version. - - [unfold p] has no effect on projection applications unless it is applied - to a constructor. If the explicit version appears it reduces to the - projection application. - - [pattern x at n], [rewrite x at n] and in general abstraction and selection - of occurrences may fail due to the disappearance of parameters. -- New universe polymorphism. +- New universe polymorphism (see reference manual) - New option -type-in-type to collapse the universe hierarchy (this makes the logic inconsistent). - The guard condition for fixpoints is now a bit stricter. Propagation of diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 6eca9fc4c2..2a976a07b3 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -282,6 +282,37 @@ the inductive type. To deactivate the printing of projections, use {\tt Unset Printing Projections}. +\subsection{Primitive Projections} +\index{Primitive projections} +\label{prim-proj} + +The option {\tt Set Primitive Projections} turns on the use of primitive +projections when defining subsequent records. Primitive projections +extended the calculus of inductive constructions with a new binary term +constructor {\tt r.(p)} representing a primitive projection p applied to +a record object {\tt r} (i.e., primitive projections are always +applied). Even if the record type has parameters, these do not appear at +applications of the projection, considerably reducing the sizes of terms +when manipulating parameterized records and typechecking time. On the +user level, primitive projections are a transparent replacement +for the usual defined ones. + + % - r.(p) and (p r) elaborate to native projection application, and + % the parameters cannot be mentioned. The following arguments are + % parsed according to the remaining implicit arguments declared for the + % projection (i.e. the implicit arguments after the record type + % argument). In dot notation, the record type argument is considered + % explicit no matter what its implicit status is. + % - r.(@p params) and @p args are parsed as regular applications of the + % projection with explicit parameters. + % - [simpl p] is forbidden, but [simpl @p] will simplify both the projection + % and its explicit [@p] version. + % - [unfold p] has no effect on projection applications unless it is applied + % to a constructor. If the explicit version appears it reduces to the + % projection application. + % - [pattern x at n], [rewrite x at n] and in general abstraction and selection + % of occurrences may fail due to the disappearance of parameters. + \section{Variants and extensions of {\mbox{\tt match}} \label{Extensions-of-match} |