diff options
author | Nadrieril | 2019-05-07 18:12:04 +0200 |
---|---|---|
committer | Nadrieril | 2019-05-07 18:12:04 +0200 |
commit | 3da450aa3fae23214aa982643b9bc4dd0ea4eaa6 (patch) | |
tree | 02e00cd008d2e7dc899b9211379596fe792f41c8 /dhall/src/error/text/IfBranchMismatch.txt | |
parent | d8a3e831fb67f86269c4baa99f9f0798a73a7247 (diff) | |
parent | 14dfeb8e7d2aa87a361a711a485243449426b144 (diff) |
Merge branch 'reorganize'
Diffstat (limited to 'dhall/src/error/text/IfBranchMismatch.txt')
-rw-r--r-- | dhall/src/error/text/IfBranchMismatch.txt | 63 |
1 files changed, 63 insertions, 0 deletions
diff --git a/dhall/src/error/text/IfBranchMismatch.txt b/dhall/src/error/text/IfBranchMismatch.txt new file mode 100644 index 0000000..a95b130 --- /dev/null +++ b/dhall/src/error/text/IfBranchMismatch.txt @@ -0,0 +1,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 |