From e5d9aee00b0c775df1d8e2d8819aeb80dffa73c2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 1 Mar 2019 17:28:19 +0100 Subject: Split abnf_to_pest and dhall into their own crates --- dhall/src/errors/IfBranchMismatch.txt | 63 +++++++++++++++++++++++++++++++++++ 1 file changed, 63 insertions(+) create mode 100644 dhall/src/errors/IfBranchMismatch.txt (limited to 'dhall/src/errors/IfBranchMismatch.txt') diff --git a/dhall/src/errors/IfBranchMismatch.txt b/dhall/src/errors/IfBranchMismatch.txt new file mode 100644 index 0000000..a95b130 --- /dev/null +++ b/dhall/src/errors/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 -- cgit v1.2.3