blob: 676647e135bfb1bb1221f0684622a75660022720 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
|
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❱
|
