diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 32 |
1 files changed, 32 insertions, 0 deletions
@@ -1,6 +1,38 @@ Changes from V8.4 ================= +Logic + +- Primitive projections for records allow for a compact representation of +projections, without parameters and avoid the behavior of defined +projections that can unfold to a case expression. To turn the use of +native projections on, use [Set Primitive Projections]. Record, Class +and Structure types defined while this option is set will be defined +with primitive projections instead of the usual encoding as a case +expression. For compatibility, when p is a primitive projection, @p can +be used to refer to the projection with explicit parameters, i.e. [@p] +is definitionaly equal to [λ params r. r.(p)]. 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 mentionned. The following arguments are + parsed according to the remaining implicits declared for the projection + (i.e. the implicits 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 it's 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. + + Vernacular commands - The command "Record foo ..." does not generate induction principles |