mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-18 18:31:43 +03:00
Wording.
This commit is contained in:
parent
d4ac7b6f52
commit
682ebbffb5
@ -1036,7 +1036,9 @@ Nested record fields can be accessed using the dot notation:
|
|||||||
x.a.b.c
|
x.a.b.c
|
||||||
map (.a.b.c) xs
|
map (.a.b.c) xs
|
||||||
|
|
||||||
There must be no spaces after the dots.
|
For the dot notation, there must be no spaces after the dots but there may be
|
||||||
|
spaces before the dots. The composite projection must be parenthesised,
|
||||||
|
otherwise ``map .a.b.c xs`` would be understood as ``map.a.b.c xs``.
|
||||||
|
|
||||||
Nested record fields can be accessed using the prefix notation, too:
|
Nested record fields can be accessed using the prefix notation, too:
|
||||||
|
|
||||||
@ -1045,7 +1047,7 @@ Nested record fields can be accessed using the prefix notation, too:
|
|||||||
(c . b . a) x
|
(c . b . a) x
|
||||||
map (c . b . a) xs
|
map (c . b . a) xs
|
||||||
|
|
||||||
Here, the spaces turn the dots into function composition operators.
|
Dots with spaces around them stand for function composition operators.
|
||||||
|
|
||||||
Nested record update
|
Nested record update
|
||||||
~~~~~~~~~~~~~~~~~~~~
|
~~~~~~~~~~~~~~~~~~~~
|
||||||
|
Loading…
Reference in New Issue
Block a user