summaryrefslogtreecommitdiff
path: root/dhall/src/error/text/InvalidPredicate.txt
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