blob: 4c15881812a321fb86bb1146daccfa3d57e50310 (
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
|
Explanation: Every ❰if❱ expression begins with a predicate which must have type
❰Bool❱
For example, these are valid ❰if❱ expressions:
┌──────────────────────────────┐
│ if True then "Yes" else "No" │
└──────────────────────────────┘
⇧
Predicate
┌─────────────────────────────────────────┐
│ λ(x : Bool) → if x then False else True │
└─────────────────────────────────────────┘
⇧
Predicate
... but these are $_NOT valid ❰if❱ expressions:
┌───────────────────────────┐
│ if 0 then "Yes" else "No" │ ❰0❱ does not have type ❰Bool❱
└───────────────────────────┘
┌────────────────────────────┐
│ if "" then False else True │ ❰""❱ does not have type ❰Bool❱
└────────────────────────────┘
Your ❰if❱ expression begins with the following predicate:
↳ $txt0
... that has type:
↳ $txt1
... but the predicate must instead have type ❰Bool❱
Some common reasons why you might get this error:
● You might be used to other programming languages that accept predicates other
than ❰Bool❱
For example, some languages permit ❰0❱ or ❰""❱ as valid predicates and treat
them as equivalent to ❰False❱. However, the Dhall language does not permit
this
|
