From 60129b7d1c0ea8bdf2ec666fa51957e97465e88f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 6 May 2019 23:17:26 +0200
Subject: Consolidate errors in the error module

---
 dhall/src/errors/NoDependentLet.txt | 76 -------------------------------------
 1 file changed, 76 deletions(-)
 delete mode 100644 dhall/src/errors/NoDependentLet.txt

(limited to 'dhall/src/errors/NoDependentLet.txt')

diff --git a/dhall/src/errors/NoDependentLet.txt b/dhall/src/errors/NoDependentLet.txt
deleted file mode 100644
index fdc65b4..0000000
--- a/dhall/src/errors/NoDependentLet.txt
+++ /dev/null
@@ -1,76 +0,0 @@
-Explanation: The Dhall programming language does not allow ❰let❱ expressions
-from terms to types.  These ❰let❱ expressions are also known as "dependent ❰let❱
-expressions" because you have a type whose value depends on the value of a term.
-
-The Dhall language forbids these dependent ❰let❱ expressions in order to
-guarantee that ❰let❱ expressions of the form:
-
-
-    ┌────────────────────┐
-    │ let x : t = r in e │
-    └────────────────────┘
-
-
-... are always equivalent to:
-
-
-    ┌──────────────────┐
-    │ (λ(x : t) → e) r │
-    └──────────────────┘
-
-
-This means that both expressions should normalize to the same result and if one
-of the two fails to type check then the other should fail to type check, too.
-
-For this reason, the following is $_NOT legal code:
-
-
-    ┌───────────────────┐
-    │ let x = 2 in Text │
-    └───────────────────┘
-
-
-... because the above ❰let❱ expression is equivalent to:
-
-
-    ┌─────────────────────────────┐
-    │ let x : Integer = 2 in Text │
-    └─────────────────────────────┘
-
-
-... which in turn must be equivalent to:
-
-
-    ┌───────────────────────────┐
-    │ (λ(x : Integer) → Text) 2 │
-    └───────────────────────────┘
-
-
-... which in turn fails to type check because this sub-expression:
-
-
-    ┌───────────────────────┐
-    │ λ(x : Integer) → Text │
-    └───────────────────────┘
-
-
-... has type:
-
-
-    ┌───────────────────────┐
-    │ ∀(x : Integer) → Text │
-    └───────────────────────┘
-
-
-... which is a forbidden dependent function type (i.e. a function from a term to
-a type).  Therefore the equivalent ❰let❱ expression is also forbidden.
-
-Your ❰let❱ expression is invalid because the input has type:
-
-↳ $txt0
-
-... and the output has kind:
-
-↳ $txt1
-
-... which makes this a forbidden dependent ❰let❱ expression
-- 
cgit v1.2.3