blob: a95b130cf24c2ee86db6692107706e7fb0a6217f (
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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
Explanation: Every ❰if❱ expression has a ❰then❱ and ❰else❱ branch, each of which
is an expression:
Expression for ❰then❱ branch
⇩
┌────────────────────────────────┐
│ if True then "Hello, world!" │
│ else "Goodbye, world!" │
└────────────────────────────────┘
⇧
Expression for ❰else❱ branch
These two expressions must have the same type. For example, the following ❰if❱
expressions are all valid:
┌──────────────────────────────────┐
│ λ(b : Bool) → if b then 0 else 1 │ Both branches have type ❰Integer❱
└──────────────────────────────────┘
┌────────────────────────────┐
│ λ(b : Bool) → │
│ if b then Natural/even │ Both branches have type ❰Natural → Bool❱
│ else Natural/odd │
└────────────────────────────┘
However, the following expression is $_NOT valid:
This branch has type ❰Integer❱
⇩
┌────────────────────────┐
│ if True then 0 │
│ else "ABC" │
└────────────────────────┘
⇧
This branch has type ❰Text❱
The ❰then❱ and ❰else❱ branches must have matching types, even if the predicate is
always ❰True❱ or ❰False❱
Your ❰if❱ expression has the following ❰then❱ branch:
↳ $txt0
... which has type:
↳ $txt2
... and the following ❰else❱ branch:
↳ $txt1
... which has a different type:
↳ $txt3
Fix your ❰then❱ and ❰else❱ branches to have matching types
|
