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 --- src/errors/InvalidListType.txt | 43 ------------------------------------------ 1 file changed, 43 deletions(-) delete mode 100644 src/errors/InvalidListType.txt (limited to 'src/errors/InvalidListType.txt') diff --git a/src/errors/InvalidListType.txt b/src/errors/InvalidListType.txt deleted file mode 100644 index 676647e..0000000 --- a/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