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/UnboundVariable.txt | 97 ++++++++++++++++++++++++++++++++++++ 1 file changed, 97 insertions(+) create mode 100644 dhall/src/errors/UnboundVariable.txt (limited to 'dhall/src/errors/UnboundVariable.txt') diff --git a/dhall/src/errors/UnboundVariable.txt b/dhall/src/errors/UnboundVariable.txt new file mode 100644 index 0000000..bd7d483 --- /dev/null +++ b/dhall/src/errors/UnboundVariable.txt @@ -0,0 +1,97 @@ +Explanation: Expressions can only reference previously introduced (i.e. "bound") +variables that are still "in scope" + +For example, the following valid expressions introduce a "bound" variable named +❰x❱: + + + ┌─────────────────┐ + │ λ(x : Bool) → x │ Anonymous functions introduce "bound" variables + └─────────────────┘ + ⇧ + This is the bound variable + + + ┌─────────────────┐ + │ let x = 1 in x │ ❰let❱ expressions introduce "bound" variables + └─────────────────┘ + ⇧ + This is the bound variable + + +However, the following expressions are not valid because they all reference a +variable that has not been introduced yet (i.e. an "unbound" variable): + + + ┌─────────────────┐ + │ λ(x : Bool) → y │ The variable ❰y❱ hasn't been introduced yet + └─────────────────┘ + ⇧ + This is the unbound variable + + + ┌──────────────────────────┐ + │ (let x = True in x) && x │ ❰x❱ is undefined outside the parentheses + └──────────────────────────┘ + ⇧ + This is the unbound variable + + + ┌────────────────┐ + │ let x = x in x │ The definition for ❰x❱ cannot reference itself + └────────────────┘ + ⇧ + This is the unbound variable + + +Some common reasons why you might get this error: + +● You misspell a variable name, like this: + + + ┌────────────────────────────────────────────────────┐ + │ λ(empty : Bool) → if emty then "Empty" else "Full" │ + └────────────────────────────────────────────────────┘ + ⇧ + Typo + + +● You misspell a reserved identifier, like this: + + + ┌──────────────────────────┐ + │ foral (a : Type) → a → a │ + └──────────────────────────┘ + ⇧ + Typo + + +● You tried to define a recursive value, like this: + + + ┌─────────────────────┐ + │ let x = x + +1 in x │ + └─────────────────────┘ + ⇧ + Recursive definitions are not allowed + + +● You accidentally forgot a ❰λ❱ or ❰∀❱/❰forall❱ + + + Unbound variable + ⇩ + ┌─────────────────┐ + │ (x : Bool) → x │ + └─────────────────┘ + ⇧ + A ❰λ❱ here would transform this into a valid anonymous function + + + Unbound variable + ⇩ + ┌────────────────────┐ + │ (x : Bool) → Bool │ + └────────────────────┘ + ⇧ + A ❰∀❱ or ❰forall❱ here would transform this into a valid function type -- cgit v1.2.3