blob: 141b96979b392c39b2e132588c77c4086bf06993 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
Explanation: You can combine records using the ❰∧❱ operator, like this:
┌───────────────────────────────────────────┐
│ { foo = 1, bar = "ABC" } ∧ { baz = True } │
└───────────────────────────────────────────┘
┌─────────────────────────────────────────────┐
│ λ(r : { foo : Bool }) → r ∧ { bar = "ABC" } │
└─────────────────────────────────────────────┘
... but you cannot combine values that are not records.
For example, the following expressions are $_NOT valid:
┌──────────────────────────────┐
│ { foo = 1, bar = "ABC" } ∧ 1 │
└──────────────────────────────┘
⇧
Invalid: Not a record
┌───────────────────────────────────────────┐
│ { foo = 1, bar = "ABC" } ∧ { baz : Bool } │
└───────────────────────────────────────────┘
⇧
Invalid: This is a record type and not a record
┌───────────────────────────────────────────┐
│ { foo = 1, bar = "ABC" } ∧ < baz = True > │
└───────────────────────────────────────────┘
⇧
Invalid: This is a union and not a record
You tried to combine the following value:
↳ $txt0
... which is not a record, but is actually a:
↳ $txt1
|
