*``foo.bar.baz`` starting with lowercase ``f`` is three lexemes: ``foo``,
``.bar``, ``.baz``
*``.foo.bar.baz`` is three lexemes: ``.foo``, ``.bar``, ``.baz``
* If you want ``Constructor.field``, you have to write ``(Constructor).field``.
* All module names must start with an uppercase letter.
New syntax of ``simpleExpr``
----------------------------
Expressions binding tighter than application (``simpleExpr``), such as variables or parenthesised expressions, have been renamed to ``simplerExpr``, and an extra layer of syntax has been inserted.
..code-block:: idris
simpleExpr ::= (.field)+ -- parses as PRecordProjection
| simplerExpr (.field)+ -- parses as PRecordFieldAccess
| simplerExpr -- (parses as whatever it used to)
*``(.foo)`` is a name, so you can use it to e.g. define a function called
``.foo`` (see ``.squared`` below)
*``(.foo.bar)`` is a parenthesised expression
Desugaring rules
----------------
*``(.field1 .field2 .field3)`` desugars to ``(\x => .field3 (.field2 (.field1
x)))``
*``(simpleExpr .field1 .field2 .field3)`` desugars to ``((.field .field2
.field3) simpleExpr)``
Record elaboration
------------------
* there is a new pragma ``%undotted_record_projections``, which is ``on`` by
default
* for every field ``f`` of a record ``R``, we get:
* projection ``f`` in namespace ``R`` (exactly like now), unless
``%undotted_record_projections`` is ``off``
* projection ``.f`` in namespace ``R`` with the same definition
Example code
------------
..code-block:: idris
record Point where
constructor MkPoint
x : Double
y : Double
This record creates two projections:
*``.x : Point -> Double``
*``.y : Point -> Double``
Because ``%undotted_record_projections`` are ``on`` by default, we also get:
*``x : Point -> Double``
*``y : Point -> Double``
To prevent cluttering the ordinary global name space with short identifiers, we can do this:
..code-block:: idris
%undotted_record_projections off
record Rect where
constructor MkRect
topLeft : Point
bottomRight : Point
For ``Rect``, we don't get the undotted projections: