diff options
author | Nadrieril | 2019-11-11 18:00:57 +0000 |
---|---|---|
committer | Nadrieril | 2019-11-11 18:00:57 +0000 |
commit | ada19118f894fbd71642ea683d9376cbbd756f7d (patch) | |
tree | 45e210c786d386182ba19d33dfe548522dbf5216 /dhall/src/error/text/TypeMismatch.txt | |
parent | 1ea6fe55eea2f1448f897e2a2805f7e0a1daac9b (diff) |
Remove unused error texts
Those were copied from dhall-haskell back before I (Nadrieril) forked
dhall-rust from Nanotech. They have never been used.
Diffstat (limited to '')
-rw-r--r-- | dhall/src/error/text/TypeMismatch.txt | 117 |
1 files changed, 0 insertions, 117 deletions
diff --git a/dhall/src/error/text/TypeMismatch.txt b/dhall/src/error/text/TypeMismatch.txt deleted file mode 100644 index 4904bf8..0000000 --- a/dhall/src/error/text/TypeMismatch.txt +++ /dev/null @@ -1,117 +0,0 @@ -Explanation: Every function declares what type or kind of argument to accept - -For example: - - - ┌───────────────────────────────┐ - │ λ(x : Bool) → x : Bool → Bool │ This anonymous function only accepts - └───────────────────────────────┘ arguments that have type ❰Bool❱ - ⇧ - The function's input type - - - ┌───────────────────────────────┐ - │ Natural/even : Natural → Bool │ This built-in function only accepts - └───────────────────────────────┘ arguments that have type ❰Natural❱ - ⇧ - The function's input type - - - ┌───────────────────────────────┐ - │ λ(a : Type) → a : Type → Type │ This anonymous function only accepts - └───────────────────────────────┘ arguments that have kind ❰Type❱ - ⇧ - The function's input kind - - - ┌────────────────────┐ - │ List : Type → Type │ This built-in function only accepts arguments that - └────────────────────┘ have kind ❰Type❱ - ⇧ - The function's input kind - - -For example, the following expressions are valid: - - - ┌────────────────────────┐ - │ (λ(x : Bool) → x) True │ ❰True❱ has type ❰Bool❱, which matches the type - └────────────────────────┘ of argument that the anonymous function accepts - - - ┌─────────────────┐ - │ Natural/even +2 │ ❰+2❱ has type ❰Natural❱, which matches the type of - └─────────────────┘ argument that the ❰Natural/even❱ function accepts, - - - ┌────────────────────────┐ - │ (λ(a : Type) → a) Bool │ ❰Bool❱ has kind ❰Type❱, which matches the kind - └────────────────────────┘ of argument that the anonymous function accepts - - - ┌───────────┐ - │ List Text │ ❰Text❱ has kind ❰Type❱, which matches the kind of argument - └───────────┘ that that the ❰List❱ function accepts - - -However, you can $_NOT apply a function to the wrong type or kind of argument - -For example, the following expressions are not valid: - - - ┌───────────────────────┐ - │ (λ(x : Bool) → x) "A" │ ❰"A"❱ has type ❰Text❱, but the anonymous function - └───────────────────────┘ expects an argument that has type ❰Bool❱ - - - ┌──────────────────┐ - │ Natural/even "A" │ ❰"A"❱ has type ❰Text❱, but the ❰Natural/even❱ function - └──────────────────┘ expects an argument that has type ❰Natural❱ - - - ┌────────────────────────┐ - │ (λ(a : Type) → a) True │ ❰True❱ has type ❰Bool❱, but the anonymous - └────────────────────────┘ function expects an argument of kind ❰Type❱ - - - ┌────────┐ - │ List 1 │ ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an - └────────┘ argument that has kind ❰Type❱ - - -You tried to invoke the following function: - -↳ $txt0 - -... which expects an argument of type or kind: - -↳ $txt1 - -... on the following argument: - -↳ $txt2 - -... which has a different type or kind: - -↳ $txt3 - -Some common reasons why you might get this error: - -● You omit a function argument by mistake: - - - ┌────────────────────────────────────────┐ - │ List/head ([1, 2, 3] : List Integer) │ - └────────────────────────────────────────┘ - ⇧ - ❰List/head❱ is missing the first argument, - which should be: ❰Integer❱ - - -● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱ - - ┌────────────────┐ - │ Natural/even 2 │ - └────────────────┘ - ⇧ - This should be ❰+2❱ |