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/InvalidListType.txt | 43 ------------------------------------ 1 file changed, 43 deletions(-) delete mode 100644 dhall/src/errors/InvalidListType.txt (limited to 'dhall/src/errors/InvalidListType.txt') diff --git a/dhall/src/errors/InvalidListType.txt b/dhall/src/errors/InvalidListType.txt deleted file mode 100644 index 676647e..0000000 --- a/dhall/src/errors/InvalidListType.txt +++ /dev/null @@ -1,43 +0,0 @@ -Explanation: Every ❰List❱ documents the type of its elements with a type -annotation, like this: - - - ┌──────────────────────────┐ - │ [1, 2, 3] : List Integer │ A ❰List❱ of three ❰Integer❱s - └──────────────────────────┘ - ⇧ - The type of the ❰List❱'s elements, which are ❰Integer❱s - - - ┌───────────────────┐ - │ [] : List Integer │ An empty ❰List❱ - └───────────────────┘ - ⇧ - You still specify the type even when the ❰List❱ is empty - - -The element type must be a type and not something else. For example, the -following element types are $_NOT valid: - - - ┌──────────────┐ - │ ... : List 1 │ - └──────────────┘ - ⇧ - This is an ❰Integer❱ and not a ❰Type❱ - - - ┌─────────────────┐ - │ ... : List Type │ - └─────────────────┘ - ⇧ - This is a ❰Kind❱ and not a ❰Type❱ - - -Even if the ❰List❱ is empty you still must specify a valid type - -You declared that the ❰List❱'s elements should have type: - -↳ $txt0 - -... which is not a ❰Type❱ -- cgit v1.2.3