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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
|
module Prelude.List (
Listdatatype `Prelude.List.List`
kind `* -> *`
executable(..)case-constant `caseList`
constructor `Nil`
constructor `(:)`
,
Consconstant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executable,
snocconstant `Prelude.List.snoc`
constant
type `List 'a -> 'a -> List 'a`
executable,
lastconstant `Prelude.List.last`
constant
type `List 'a -> Maybe 'a`
executable,
mapconstant `Prelude.List.map`
constant
type `('a -> 'b) -> List 'a -> List 'b`
executable,
(++)constant `Prelude.List.(++)`
constant
type `List 'a -> List 'a -> List 'a`
executable,
filterconstant `Prelude.List.filter`
constant
type `('a -> Bool) -> List 'a -> List 'a`
executable,
partitionconstant `Prelude.List.partition`
constant
type `('a -> Bool) -> List 'a -> (List 'a, List 'a)`
executable,
removeFirstconstant `Prelude.List.removeFirst`
constant
type `('a -> Bool) -> List 'a -> List 'a`
executable,
takeFirstconstant `Prelude.List.takeFirst`
constant
type `('a -> Bool) -> List 'a -> Maybe (List 'a, 'a)`
executable,
concatconstant `Prelude.List.concat`
constant
type `List (List 'a) -> List 'a`
executable,
concatMapconstant `Prelude.List.concatMap`
constant
type `('a -> List 'b) -> List 'a -> List 'b`
executable,
nullconstant `Prelude.List.null`
constant
type `List 'a -> Bool`
executable,
lengthconstant `Prelude.List.length`
constant
type `List 'a -> Natural`
executable,
countconstant `Prelude.List.count`
constant
type `Eq 'a => 'a -> List 'a -> Natural`
executable,
foldlconstant `Prelude.List.foldl`
constant
type `('a -> 'b -> 'a) -> 'a -> List 'b -> 'a`
executable, foldrconstant `Prelude.List.foldr`
constant
type `('a -> 'b -> 'b) -> 'b -> List 'a -> 'b`
executable, foldlWithAbortconstant `Prelude.List.foldlWithAbort`
constant
type `('a -> Bool) -> ('a -> 'b -> 'a) -> 'a -> List 'b -> 'a`
executable,
scanlconstant `Prelude.List.scanl`
constant
type `('a -> 'b -> 'a) -> 'a -> List 'b -> List 'a`
executable, scanrconstant `Prelude.List.scanr`
constant
type `('a -> 'b -> 'b) -> 'b -> List 'a -> List 'b`
executable,
reverseconstant `Prelude.List.reverse`
constant
type `List 'a -> List 'a`
executable,
revAppendconstant `Prelude.List.revAppend`
constant
type `List 'a -> List 'a -> List 'a`
executable,
andconstant `Prelude.List.and`
constant
type `List Bool -> Bool`
executable,
orconstant `Prelude.List.or`
constant
type `List Bool -> Bool`
executable,
allconstant `Prelude.List.all`
constant
type `('a -> Bool) -> List 'a -> Bool`
executable,
anyconstant `Prelude.List.any`
constant
type `('a -> Bool) -> List 'a -> Bool`
executable,
elemconstant `Prelude.List.elem`
constant
type `Eq 'a => 'a -> List 'a -> Bool`
executable,
notElemconstant `Prelude.List.notElem`
constant
type `Eq 'a => 'a -> List 'a -> Bool`
executable,
andPconstant `Prelude.List.andP`
constant
type `List Prop -> Prop`
non-executable,
orPconstant `Prelude.List.orP`
constant
type `List Prop -> Prop`
non-executable,
allPconstant `Prelude.List.allP`
constant
type `('a -> Prop) -> List 'a -> Prop`
non-executable,
anyPconstant `Prelude.List.anyP`
constant
type `('a -> Prop) -> List 'a -> Prop`
non-executable,
elemPconstant `Prelude.List.elemP`
constant
type `EqP 'a => 'a -> List 'a -> Prop`
non-executable,
notElemPconstant `Prelude.List.notElemP`
constant
type `EqP 'a => 'a -> List 'a -> Prop`
non-executable,
nubconstant `Prelude.List.nub`
constant
type `Eq 'a => List 'a -> List 'a`
executable,
nubByconstant `Prelude.List.nubBy`
constant
type `('a -> 'a -> Bool) -> List 'a -> List 'a`
executable
) where
{-# NoImplicitPrelude #-}
{-# allow-similar-names "foldl", "foldr", "scanl", "scanr" #-}
import Prelude.Bool
import Prelude.Num
import Prelude.Function
import Prelude.Default
import Prelude.Eq
import Prelude.Ord
import Prelude.Functor
import Prelude.Maybe hiding (mapconstant `Prelude.Maybe.map`
constant
type `('a -> 'b) -> Maybe 'a -> Maybe 'b`
executable)
{-# naming-convention constructor - #-}
datatype rec Listdatatype `Prelude.List.List`
kind `* -> *`
executable 'atype-variable `'a`
kind `*` := Nil | (:) 'atype-variable `'a`
kind `*` (Listdatatype `Prelude.List.List`
kind `* -> *`
executable 'atype-variable `'a`
kind `*`)
{-# naming-convention constructor reset #-}
alias Cons := (:)constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executable
instance Defaulttype-class `Prelude.Default.Default`
arguments: ('a :: *)
has default derive templates ['atype-variable `'a`
kind `*`] where
define defaultconstant `Prelude.Default.default`
constant of type-class instance `Default (List 'a)`
type `List 'a`
executable := []
end-instance
declare mapconstant `Prelude.List.map`
constant
type `('a -> 'b) -> List 'a -> List 'b`
executable :: ('atype-variable `'a`
kind `*` -> 'btype-variable `'b`
kind `*`) -> ['atype-variable `'a`
kind `*`] -> ['btype-variable `'b`
kind `*`]
define rec mapconstant `Prelude.List.map`
constant
type `('a -> 'b) -> List 'a -> List 'b`
executable _ [] := []
| mapconstant `Prelude.List.map`
constant
type `('a -> 'b) -> List 'a -> List 'b`
executable fvariable `f`
type `'a -> 'b` (xvariable `x`
type `'a` :constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executable xsvariable `xs`
type `List 'a`) := (fvariable `f`
type `'a -> 'b` xvariable `x`
type `'a`) :constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
type in context `'b -> List 'b -> List 'b`
executable (mapconstant `Prelude.List.map` (recursive usage)
constant
type `('a -> 'b) -> List 'a -> List 'b`
executable fvariable `f`
type `'a -> 'b` xsvariable `xs`
type `List 'a`)
instance Functortype-class `Prelude.Functor.Functor`
arguments: ('F :: * -> *)
reserved var-names: 'a, 'b
statically-resolved Listdatatype `Prelude.List.List`
kind `* -> *`
executable where
define fmapconstant `Prelude.Functor.fmap`
constant of type-class instance `Functor List`
type `('a -> 'b) -> List 'a -> List 'b`
executable := mapconstant `Prelude.List.map`
constant
type `('a -> 'b) -> List 'a -> List 'b`
executable
{-# inline fmapconstant `Prelude.Functor.fmap`
constant of type-class instance `Functor List`
type `('a -> 'b) -> List 'a -> List 'b`
executable #-}
end-instance
declare (++)constant `Prelude.List.(++)`
constant
type `List 'a -> List 'a -> List 'a`
executable :: ['atype-variable `'a`
kind `*`] -> ['atype-variable `'a`
kind `*`] -> ['atype-variable `'a`
kind `*`]
define rec (++)constant `Prelude.List.(++)`
constant
type `List 'a -> List 'a -> List 'a`
executable [] ysvariable `ys`
type `List 'a` := ysvariable `ys`
type `List 'a`
| (++)constant `Prelude.List.(++)`
constant
type `List 'a -> List 'a -> List 'a`
executable (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executablexsvariable `xs`
type `List 'a`) ysvariable `ys`
type `List 'a` := xvariable `x`
type `'a` :constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executable (xsvariable `xs`
type `List 'a` ++constant `Prelude.List.(++)` (recursive usage)
constant
type `List 'a -> List 'a -> List 'a`
executable ysvariable `ys`
type `List 'a`)
declare snocconstant `Prelude.List.snoc`
constant
type `List 'a -> 'a -> List 'a`
executable :: ['atype-variable `'a`
kind `*`] -> 'atype-variable `'a`
kind `*` -> ['atype-variable `'a`
kind `*`]
define rec snocconstant `Prelude.List.snoc`
constant
type `List 'a -> 'a -> List 'a`
executable [] yvariable `y`
type `'a` := [yvariable `y`
type `'a`]
| snocconstant `Prelude.List.snoc`
constant
type `List 'a -> 'a -> List 'a`
executable (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executablexsvariable `xs`
type `List 'a`) yvariable `y`
type `'a` := xvariable `x`
type `'a` :constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executable (snocconstant `Prelude.List.snoc` (recursive usage)
constant
type `List 'a -> 'a -> List 'a`
executable xsvariable `xs`
type `List 'a` yvariable `y`
type `'a`)
declare lastconstant `Prelude.List.last`
constant
type `List 'a -> Maybe 'a`
executable :: ['atype-variable `'a`
kind `*`] -> Maybedatatype `Prelude.Maybe.Maybe`
kind `* -> *`
executable 'atype-variable `'a`
kind `*`
define rec lastconstant `Prelude.List.last`
constant
type `List 'a -> Maybe 'a`
executable [] := Nothingconstant `Prelude.Maybe.Nothing`
constructor of datatype `Maybe`
type `Maybe 'a`
executable
| lastconstant `Prelude.List.last`
constant
type `List 'a -> Maybe 'a`
executable [xvariable `x`
type `'a`] := Justconstant `Prelude.Maybe.Just`
constructor of datatype `Maybe`
type `'a -> Maybe 'a`
executable xvariable `x`
type `'a`
| lastconstant `Prelude.List.last`
constant
type `List 'a -> Maybe 'a`
executable (_:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executablexvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executablexsvariable `xs`
type `List 'a`) := lastconstant `Prelude.List.last` (recursive usage)
constant
type `List 'a -> Maybe 'a`
executable (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executablexsvariable `xs`
type `List 'a`)
declare destSnocconstant `Prelude.List.destSnoc`
constant
type `List 'a -> Maybe (List 'a, 'a)`
executable :: ['atype-variable `'a`
kind `*`] -> Maybedatatype `Prelude.Maybe.Maybe`
kind `* -> *`
executable (['atype-variable `'a`
kind `*`], 'atype-variable `'a`
kind `*`)
define rec destSnocconstant `Prelude.List.destSnoc`
constant
type `List 'a -> Maybe (List 'a, 'a)`
executable [] := Nothingconstant `Prelude.Maybe.Nothing`
constructor of datatype `Maybe`
type `Maybe 'a`
type in context `Maybe (List 'a, 'a)`
executable
| destSnocconstant `Prelude.List.destSnoc`
constant
type `List 'a -> Maybe (List 'a, 'a)`
executable (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executablexsvariable `xs`
type `List 'a`) :=
case destSnocconstant `Prelude.List.destSnoc` (recursive usage)
constant
type `List 'a -> Maybe (List 'a, 'a)`
executable xsvariable `xs`
type `List 'a` of
Nothingconstant `Prelude.Maybe.Nothing`
constructor of datatype `Maybe`
type `Maybe 'a`
type in context `Maybe (List 'a, 'a)`
executable -> Justconstant `Prelude.Maybe.Just`
constructor of datatype `Maybe`
type `'a -> Maybe 'a`
type in context `(List 'a, 'a) -> Maybe (List 'a, 'a)`
executable ([], xvariable `x`
type `'a`)
| Justconstant `Prelude.Maybe.Just`
constructor of datatype `Maybe`
type `'a -> Maybe 'a`
type in context `(List 'a, 'a) -> Maybe (List 'a, 'a)`
executable (ysvariable `ys`
type `List 'a`, yvariable `y`
type `'a`) -> Justconstant `Prelude.Maybe.Just`
constructor of datatype `Maybe`
type `'a -> Maybe 'a`
type in context `(List 'a, 'a) -> Maybe (List 'a, 'a)`
executable (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executableysvariable `ys`
type `List 'a`, yvariable `y`
type `'a`)
end
declare caseListSnocconstant `Prelude.List.caseListSnoc`
constant
type `'a -> (List 'c -> 'c -> 'a) -> List 'c -> 'a`
executable :: 'atype-variable `'a`
kind `*` -> (['ctype-variable `'c`
kind `*`] -> 'ctype-variable `'c`
kind `*` -> 'atype-variable `'a`
kind `*`) -> ['ctype-variable `'c`
kind `*`] -> 'atype-variable `'a`
kind `*`
define caseListSnocconstant `Prelude.List.caseListSnoc`
constant
type `'a -> (List 'c -> 'c -> 'a) -> List 'c -> 'a`
executable nilVvariable `nilV`
type `'a` snocVvariable `snocV`
type `List 'c -> 'c -> 'a` lvariable `l`
type `List 'c` :=
case (destSnocconstant `Prelude.List.destSnoc`
constant
type `List 'a -> Maybe (List 'a, 'a)`
type in context `List 'c -> Maybe (List 'c, 'c)`
executable lvariable `l`
type `List 'c`) of
Nothingconstant `Prelude.Maybe.Nothing`
constructor of datatype `Maybe`
type `Maybe 'a`
type in context `Maybe (List 'c, 'c)`
executable -> nilVvariable `nilV`
type `'a`
| Justconstant `Prelude.Maybe.Just`
constructor of datatype `Maybe`
type `'a -> Maybe 'a`
type in context `(List 'c, 'c) -> Maybe (List 'c, 'c)`
executable (xsvariable `xs`
type `List 'c`, xvariable `x`
type `'c`) -> snocVvariable `snocV`
type `List 'c -> 'c -> 'a` xsvariable `xs`
type `List 'c` xvariable `x`
type `'c`
end
constructor-family caseListSnocconstant `Prelude.List.caseListSnoc`
constant
type `'a -> (List 'c -> 'c -> 'a) -> List 'c -> 'a`
executable (Nilconstant `Prelude.List.Nil`
constructor of datatype `List`
type `List 'a`
executable, snocconstant `Prelude.List.snoc`
constant
type `List 'a -> 'a -> List 'a`
executable)
declare filterconstant `Prelude.List.filter`
constant
type `('a -> Bool) -> List 'a -> List 'a`
executable :: ('atype-variable `'a`
kind `*` -> Booldatatype `Prelude.Bool.Bool`
kind `*`
executable) -> Listdatatype `Prelude.List.List`
kind `* -> *`
executable 'atype-variable `'a`
kind `*` -> Listdatatype `Prelude.List.List`
kind `* -> *`
executable 'atype-variable `'a`
kind `*`
define rec filterconstant `Prelude.List.filter`
constant
type `('a -> Bool) -> List 'a -> List 'a`
executable _ [] := []
| filterconstant `Prelude.List.filter`
constant
type `('a -> Bool) -> List 'a -> List 'a`
executable pvariable `p`
type `'a -> Bool` (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executablexsvariable `xs`
type `List 'a`) :=
if (pvariable `p`
type `'a -> Bool` xvariable `x`
type `'a`) then (xvariable `x`
type `'a` :constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executable (filterconstant `Prelude.List.filter` (recursive usage)
constant
type `('a -> Bool) -> List 'a -> List 'a`
executable pvariable `p`
type `'a -> Bool` xsvariable `xs`
type `List 'a`)) else filterconstant `Prelude.List.filter` (recursive usage)
constant
type `('a -> Bool) -> List 'a -> List 'a`
executable pvariable `p`
type `'a -> Bool` xsvariable `xs`
type `List 'a`
declare partitionconstant `Prelude.List.partition`
constant
type `('a -> Bool) -> List 'a -> (List 'a, List 'a)`
executable :: ('atype-variable `'a`
kind `*` -> Booldatatype `Prelude.Bool.Bool`
kind `*`
executable) -> Listdatatype `Prelude.List.List`
kind `* -> *`
executable 'atype-variable `'a`
kind `*` -> (Listdatatype `Prelude.List.List`
kind `* -> *`
executable 'atype-variable `'a`
kind `*`, Listdatatype `Prelude.List.List`
kind `* -> *`
executable 'atype-variable `'a`
kind `*`)
define rec partitionconstant `Prelude.List.partition`
constant
type `('a -> Bool) -> List 'a -> (List 'a, List 'a)`
executable _ [] := ([], [])
| partitionconstant `Prelude.List.partition`
constant
type `('a -> Bool) -> List 'a -> (List 'a, List 'a)`
executable pvariable `p`
type `'a -> Bool` (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executablexsvariable `xs`
type `List 'a`) :=
let
val (ltvariable `lt`
type `List 'a`, lfvariable `lf`
type `List 'a`) = partitionconstant `Prelude.List.partition` (recursive usage)
constant
type `('a -> Bool) -> List 'a -> (List 'a, List 'a)`
executable pvariable `p`
type `'a -> Bool` xsvariable `xs`
type `List 'a`
in
if pvariable `p`
type `'a -> Bool` xvariable `x`
type `'a` then (xvariable `x`
type `'a` :constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executable ltvariable `lt`
type `List 'a`, lfvariable `lf`
type `List 'a`) else (ltvariable `lt`
type `List 'a`, xvariable `x`
type `'a` :constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executable lfvariable `lf`
type `List 'a`)
end
declare takeFirstconstant `Prelude.List.takeFirst`
constant
type `('a -> Bool) -> List 'a -> Maybe (List 'a, 'a)`
executable :: ('atype-variable `'a`
kind `*` -> Booldatatype `Prelude.Bool.Bool`
kind `*`
executable) -> Listdatatype `Prelude.List.List`
kind `* -> *`
executable 'atype-variable `'a`
kind `*` -> Maybedatatype `Prelude.Maybe.Maybe`
kind `* -> *`
executable (Listdatatype `Prelude.List.List`
kind `* -> *`
executable 'atype-variable `'a`
kind `*`, 'atype-variable `'a`
kind `*`)
define takeFirstconstant `Prelude.List.takeFirst`
constant
type `('a -> Bool) -> List 'a -> Maybe (List 'a, 'a)`
executable pvariable `p`
type `'a -> Bool` := takeFirstAccconstant `Prelude.List.takeFirstAcc`
constant
type `('a -> Bool) -> List 'a -> List 'a -> Maybe (List 'a, 'a)`
executable pvariable `p`
type `'a -> Bool` []
declare takeFirstAccconstant `Prelude.List.takeFirstAcc`
constant
type `('a -> Bool) -> List 'a -> List 'a -> Maybe (List 'a, 'a)`
executable :: ('atype-variable `'a`
kind `*` -> Booldatatype `Prelude.Bool.Bool`
kind `*`
executable) -> Listdatatype `Prelude.List.List`
kind `* -> *`
executable 'atype-variable `'a`
kind `*` -> Listdatatype `Prelude.List.List`
kind `* -> *`
executable 'atype-variable `'a`
kind `*` -> Maybedatatype `Prelude.Maybe.Maybe`
kind `* -> *`
executable (Listdatatype `Prelude.List.List`
kind `* -> *`
executable 'atype-variable `'a`
kind `*`, 'atype-variable `'a`
kind `*`)
define rec takeFirstAccconstant `Prelude.List.takeFirstAcc`
constant
type `('a -> Bool) -> List 'a -> List 'a -> Maybe (List 'a, 'a)`
executable _ _ [] := Nothingconstant `Prelude.Maybe.Nothing`
constructor of datatype `Maybe`
type `Maybe 'a`
type in context `Maybe (List 'a, 'a)`
executable
| takeFirstAccconstant `Prelude.List.takeFirstAcc`
constant
type `('a -> Bool) -> List 'a -> List 'a -> Maybe (List 'a, 'a)`
executable pvariable `p`
type `'a -> Bool` accvariable `acc`
type `List 'a` (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executablexsvariable `xs`
type `List 'a`) :=
if pvariable `p`
type `'a -> Bool` xvariable `x`
type `'a` then Justconstant `Prelude.Maybe.Just`
constructor of datatype `Maybe`
type `'a -> Maybe 'a`
type in context `(List 'a, 'a) -> Maybe (List 'a, 'a)`
executable (reverseconstant `Prelude.List.reverse`
constant
type `List 'a -> List 'a`
executable accvariable `acc`
type `List 'a` ++constant `Prelude.List.(++)`
constant
type `List 'a -> List 'a -> List 'a`
executable xsvariable `xs`
type `List 'a`, xvariable `x`
type `'a`) else
takeFirstAccconstant `Prelude.List.takeFirstAcc` (recursive usage)
constant
type `('a -> Bool) -> List 'a -> List 'a -> Maybe (List 'a, 'a)`
executable pvariable `p`
type `'a -> Bool` (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executableaccvariable `acc`
type `List 'a`) xsvariable `xs`
type `List 'a`
declare removeFirstconstant `Prelude.List.removeFirst`
constant
type `('a -> Bool) -> List 'a -> List 'a`
executable :: ('atype-variable `'a`
kind `*` -> Booldatatype `Prelude.Bool.Bool`
kind `*`
executable) -> Listdatatype `Prelude.List.List`
kind `* -> *`
executable 'atype-variable `'a`
kind `*` -> Listdatatype `Prelude.List.List`
kind `* -> *`
executable 'atype-variable `'a`
kind `*`
define removeFirstconstant `Prelude.List.removeFirst`
constant
type `('a -> Bool) -> List 'a -> List 'a`
executable pvariable `p`
type `'a -> Bool` lvariable `l`
type `List 'a` := case takeFirstconstant `Prelude.List.takeFirst`
constant
type `('a -> Bool) -> List 'a -> Maybe (List 'a, 'a)`
executable pvariable `p`
type `'a -> Bool` lvariable `l`
type `List 'a` of
Nothingconstant `Prelude.Maybe.Nothing`
constructor of datatype `Maybe`
type `Maybe 'a`
type in context `Maybe (List 'a, 'a)`
executable -> lvariable `l`
type `List 'a`
| Justconstant `Prelude.Maybe.Just`
constructor of datatype `Maybe`
type `'a -> Maybe 'a`
type in context `(List 'a, 'a) -> Maybe (List 'a, 'a)`
executable (l'variable `l'`
type `List 'a`, _) -> l'variable `l'`
type `List 'a`
end
declare concatconstant `Prelude.List.concat`
constant
type `List (List 'a) -> List 'a`
executable :: [['atype-variable `'a`
kind `*`]] -> ['atype-variable `'a`
kind `*`]
define concatconstant `Prelude.List.concat`
constant
type `List (List 'a) -> List 'a`
executable xssvariable `xss`
type `List (List 'a)` := foldrconstant `Prelude.List.foldr`
constant
type `('a -> 'b -> 'b) -> 'b -> List 'a -> 'b`
type in context `(List 'a -> List 'a -> List 'a) -> List 'a -> List (List 'a) -> List 'a`
executable (++)constant `Prelude.List.(++)`
constant
type `List 'a -> List 'a -> List 'a`
executable [] xssvariable `xss`
type `List (List 'a)`
declare concatMapconstant `Prelude.List.concatMap`
constant
type `('a -> List 'b) -> List 'a -> List 'b`
executable :: ('atype-variable `'a`
kind `*` -> ['btype-variable `'b`
kind `*`]) -> ['atype-variable `'a`
kind `*`] -> ['btype-variable `'b`
kind `*`]
define concatMapconstant `Prelude.List.concatMap`
constant
type `('a -> List 'b) -> List 'a -> List 'b`
executable fvariable `f`
type `'a -> List 'b` := concatconstant `Prelude.List.concat`
constant
type `List (List 'a) -> List 'a`
type in context `List (List 'b) -> List 'b`
executable .constant `Prelude.Function.(.)`
constant of type-class `Dot`
type `'a -> 'b -> 'c`
type in context `(List (List 'b) -> List 'b) -> (List 'a -> List (List 'b)) -> List 'a -> List 'b`
executable
statically resolved type-class instance (mapconstant `Prelude.List.map`
constant
type `('a -> 'b) -> List 'a -> List 'b`
type in context `('a -> List 'b) -> List 'a -> List (List 'b)`
executable fvariable `f`
type `'a -> List 'b`)
declare nullconstant `Prelude.List.null`
constant
type `List 'a -> Bool`
executable :: ['atype-variable `'a`
kind `*`] -> Booldatatype `Prelude.Bool.Bool`
kind `*`
executable
define nullconstant `Prelude.List.null`
constant
type `List 'a -> Bool`
executable [] := Trueconstant `Prelude.Bool.True`
constructor of datatype `Bool`
type `Bool`
executable
| nullconstant `Prelude.List.null`
constant
type `List 'a -> Bool`
executable (_:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executable_) := Falseconstant `Prelude.Bool.False`
constructor of datatype `Bool`
type `Bool`
executable
declare foldlconstant `Prelude.List.foldl`
constant
type `('a -> 'b -> 'a) -> 'a -> List 'b -> 'a`
executable :: ('atype-variable `'a`
kind `*` -> 'btype-variable `'b`
kind `*` -> 'atype-variable `'a`
kind `*`) -> 'atype-variable `'a`
kind `*` -> ['btype-variable `'b`
kind `*`] -> 'atype-variable `'a`
kind `*`
define rec foldlconstant `Prelude.List.foldl`
constant
type `('a -> 'b -> 'a) -> 'a -> List 'b -> 'a`
executable _ zvariable `z`
type `'a` [] := zvariable `z`
type `'a`
| foldlconstant `Prelude.List.foldl`
constant
type `('a -> 'b -> 'a) -> 'a -> List 'b -> 'a`
executable fvariable `f`
type `'a -> 'b -> 'a` zvariable `z`
type `'a` (xvariable `x`
type `'b`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
type in context `'b -> List 'b -> List 'b`
executablexsvariable `xs`
type `List 'b`) := foldlconstant `Prelude.List.foldl` (recursive usage)
constant
type `('a -> 'b -> 'a) -> 'a -> List 'b -> 'a`
executable fvariable `f`
type `'a -> 'b -> 'a` (fvariable `f`
type `'a -> 'b -> 'a` zvariable `z`
type `'a` xvariable `x`
type `'b`) xsvariable `xs`
type `List 'b`
declare foldlWithAbortconstant `Prelude.List.foldlWithAbort`
constant
type `('a -> Bool) -> ('a -> 'b -> 'a) -> 'a -> List 'b -> 'a`
executable :: ('atype-variable `'a`
kind `*` -> Booldatatype `Prelude.Bool.Bool`
kind `*`
executable) -> ('atype-variable `'a`
kind `*` -> 'btype-variable `'b`
kind `*` -> 'atype-variable `'a`
kind `*`) -> 'atype-variable `'a`
kind `*` -> ['btype-variable `'b`
kind `*`] -> 'atype-variable `'a`
kind `*`
define rec foldlWithAbortconstant `Prelude.List.foldlWithAbort`
constant
type `('a -> Bool) -> ('a -> 'b -> 'a) -> 'a -> List 'b -> 'a`
executable _ _ zvariable `z`
type `'a` [] := zvariable `z`
type `'a`
| foldlWithAbortconstant `Prelude.List.foldlWithAbort`
constant
type `('a -> Bool) -> ('a -> 'b -> 'a) -> 'a -> List 'b -> 'a`
executable abvariable `ab`
type `'a -> Bool` fvariable `f`
type `'a -> 'b -> 'a` zvariable `z`
type `'a` (xvariable `x`
type `'b`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
type in context `'b -> List 'b -> List 'b`
executablexsvariable `xs`
type `List 'b`) :=
if (abvariable `ab`
type `'a -> Bool` zvariable `z`
type `'a`) then zvariable `z`
type `'a` else foldlWithAbortconstant `Prelude.List.foldlWithAbort` (recursive usage)
constant
type `('a -> Bool) -> ('a -> 'b -> 'a) -> 'a -> List 'b -> 'a`
executable abvariable `ab`
type `'a -> Bool` fvariable `f`
type `'a -> 'b -> 'a` (fvariable `f`
type `'a -> 'b -> 'a` zvariable `z`
type `'a` xvariable `x`
type `'b`) xsvariable `xs`
type `List 'b`
declare scanlconstant `Prelude.List.scanl`
constant
type `('a -> 'b -> 'a) -> 'a -> List 'b -> List 'a`
executable :: ('atype-variable `'a`
kind `*` -> 'btype-variable `'b`
kind `*` -> 'atype-variable `'a`
kind `*`) -> 'atype-variable `'a`
kind `*` -> ['btype-variable `'b`
kind `*`] -> ['atype-variable `'a`
kind `*`]
define rec scanlconstant `Prelude.List.scanl`
constant
type `('a -> 'b -> 'a) -> 'a -> List 'b -> List 'a`
executable _ qvariable `q`
type `'a` [] := [qvariable `q`
type `'a`]
| scanlconstant `Prelude.List.scanl`
constant
type `('a -> 'b -> 'a) -> 'a -> List 'b -> List 'a`
executable fvariable `f`
type `'a -> 'b -> 'a` qvariable `q`
type `'a` (xvariable `x`
type `'b`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
type in context `'b -> List 'b -> List 'b`
executablexsvariable `xs`
type `List 'b`) := qvariable `q`
type `'a` :constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executable (scanlconstant `Prelude.List.scanl` (recursive usage)
constant
type `('a -> 'b -> 'a) -> 'a -> List 'b -> List 'a`
executable fvariable `f`
type `'a -> 'b -> 'a` (fvariable `f`
type `'a -> 'b -> 'a` qvariable `q`
type `'a` xvariable `x`
type `'b`) xsvariable `xs`
type `List 'b`)
declare foldrconstant `Prelude.List.foldr`
constant
type `('a -> 'b -> 'b) -> 'b -> List 'a -> 'b`
executable :: ('atype-variable `'a`
kind `*` -> 'btype-variable `'b`
kind `*` -> 'btype-variable `'b`
kind `*`) -> 'btype-variable `'b`
kind `*` -> ['atype-variable `'a`
kind `*`] -> 'btype-variable `'b`
kind `*`
define rec foldrconstant `Prelude.List.foldr`
constant
type `('a -> 'b -> 'b) -> 'b -> List 'a -> 'b`
executable _ zvariable `z`
type `'b` [] := zvariable `z`
type `'b`
| foldrconstant `Prelude.List.foldr`
constant
type `('a -> 'b -> 'b) -> 'b -> List 'a -> 'b`
executable fvariable `f`
type `'a -> 'b -> 'b` zvariable `z`
type `'b` (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executablexsvariable `xs`
type `List 'a`) := fvariable `f`
type `'a -> 'b -> 'b` xvariable `x`
type `'a` (foldrconstant `Prelude.List.foldr` (recursive usage)
constant
type `('a -> 'b -> 'b) -> 'b -> List 'a -> 'b`
executable fvariable `f`
type `'a -> 'b -> 'b` zvariable `z`
type `'b` xsvariable `xs`
type `List 'a`)
declare scanrconstant `Prelude.List.scanr`
constant
type `('a -> 'b -> 'b) -> 'b -> List 'a -> List 'b`
executable :: ('atype-variable `'a`
kind `*` -> 'btype-variable `'b`
kind `*` -> 'btype-variable `'b`
kind `*`) -> 'btype-variable `'b`
kind `*` -> ['atype-variable `'a`
kind `*`] -> ['btype-variable `'b`
kind `*`]
define rec scanrconstant `Prelude.List.scanr`
constant
type `('a -> 'b -> 'b) -> 'b -> List 'a -> List 'b`
executable _ q0variable `q0`
type `'b` [] := [q0variable `q0`
type `'b`]
| scanrconstant `Prelude.List.scanr`
constant
type `('a -> 'b -> 'b) -> 'b -> List 'a -> List 'b`
executable fvariable `f`
type `'a -> 'b -> 'b` q0variable `q0`
type `'b` (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executablexsvariable `xs`
type `List 'a`) :=
case (scanrconstant `Prelude.List.scanr` (recursive usage)
constant
type `('a -> 'b -> 'b) -> 'b -> List 'a -> List 'b`
executable fvariable `f`
type `'a -> 'b -> 'b` q0variable `q0`
type `'b` xsvariable `xs`
type `List 'a`) of
[] -> unreachableconstant `Prelude.Default.unreachable`
constant
type `Default 'a => 'a`
type in context `List 'b`
executable
| qvariable `q`
type `'b` :constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
type in context `'b -> List 'b -> List 'b`
executable qsvariable `qs`
type `List 'b` -> (fvariable `f`
type `'a -> 'b -> 'b` xvariable `x`
type `'a` qvariable `q`
type `'b`) :constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
type in context `'b -> List 'b -> List 'b`
executable (qvariable `q`
type `'b` :constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
type in context `'b -> List 'b -> List 'b`
executable qsvariable `qs`
type `List 'b`)
end
declare lengthconstant `Prelude.List.length`
constant
type `List 'a -> Natural`
executable :: ['atype-variable `'a`
kind `*`] -> Naturaldatatype `Prelude.Num.Natural`
kind `*`
executable
define lengthconstant `Prelude.List.length`
constant
type `List 'a -> Natural`
executable := foldlconstant `Prelude.List.foldl`
constant
type `('a -> 'b -> 'a) -> 'a -> List 'b -> 'a`
type in context `(Natural -> 'a -> Natural) -> Natural -> List 'a -> Natural`
executable (fntype `Natural -> 'a -> Natural` cvariable `c`
type `Natural` _ -> cvariable `c`
type `Natural` +constant `Prelude.Num.(+)`
constant of type-class `NumPlus`
type `'a -> 'a -> 'a`
type in context `Natural -> Natural -> Natural`
executable
statically resolved type-class instance 1natural number literal
type `Natural`
decimal value: 1
hexadecimal value: 0x1
octal value: 0o1
binary value: 0b1) 0natural number literal
type `Natural`
decimal value: 0
hexadecimal value: 0x0
octal value: 0o0
binary value: 0b0
declare countconstant `Prelude.List.count`
constant
type `Eq 'a => 'a -> List 'a -> Natural`
executable :: Eqtype-class `Prelude.Eq.Eq`
arguments: ('a :: *)
super-class constraints:
- Prelude.Eq.EqP 'a
has default derive templates 'atype-variable `'a`
kind `*` => 'atype-variable `'a`
kind `*` -> ['atype-variable `'a`
kind `*`] -> Naturaldatatype `Prelude.Num.Natural`
kind `*`
executable
define countconstant `Prelude.List.count`
constant
type `Eq 'a => 'a -> List 'a -> Natural`
executable evariable `e`
type `'a` := foldlconstant `Prelude.List.foldl`
constant
type `('a -> 'b -> 'a) -> 'a -> List 'b -> 'a`
type in context `(Natural -> 'a -> Natural) -> Natural -> List 'a -> Natural`
executable (fntype `Natural -> 'a -> Natural` cvariable `c`
type `Natural` e'variable `e'`
type `'a` -> if (evariable `e`
type `'a` ==constant `Prelude.Eq.(==)`
constant of type-class `Eq`
type `'a -> 'a -> Bool`
executable
type-class instance from argument e'variable `e'`
type `'a`) then cvariable `c`
type `Natural` +constant `Prelude.Num.(+)`
constant of type-class `NumPlus`
type `'a -> 'a -> 'a`
type in context `Natural -> Natural -> Natural`
executable
statically resolved type-class instance 1natural number literal
type `Natural`
decimal value: 1
hexadecimal value: 0x1
octal value: 0o1
binary value: 0b1 else cvariable `c`
type `Natural`) 0natural number literal
type `Natural`
decimal value: 0
hexadecimal value: 0x0
octal value: 0o0
binary value: 0b0
declare revAppendconstant `Prelude.List.revAppend`
constant
type `List 'a -> List 'a -> List 'a`
executable :: ['atype-variable `'a`
kind `*`] -> ['atype-variable `'a`
kind `*`] -> ['atype-variable `'a`
kind `*`]
define rec revAppendconstant `Prelude.List.revAppend`
constant
type `List 'a -> List 'a -> List 'a`
executable accvariable `acc`
type `List 'a` [] := accvariable `acc`
type `List 'a`
| revAppendconstant `Prelude.List.revAppend`
constant
type `List 'a -> List 'a -> List 'a`
executable accvariable `acc`
type `List 'a` (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executablexsvariable `xs`
type `List 'a`) := revAppendconstant `Prelude.List.revAppend` (recursive usage)
constant
type `List 'a -> List 'a -> List 'a`
executable (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executableaccvariable `acc`
type `List 'a`) xsvariable `xs`
type `List 'a`
declare reverseconstant `Prelude.List.reverse`
constant
type `List 'a -> List 'a`
executable :: ['atype-variable `'a`
kind `*`] -> ['atype-variable `'a`
kind `*`]
define reverseconstant `Prelude.List.reverse`
constant
type `List 'a -> List 'a`
executable := revAppendconstant `Prelude.List.revAppend`
constant
type `List 'a -> List 'a -> List 'a`
executable []
declare andconstant `Prelude.List.and`
constant
type `List Bool -> Bool`
executable :: [Booldatatype `Prelude.Bool.Bool`
kind `*`
executable] -> Booldatatype `Prelude.Bool.Bool`
kind `*`
executable
define rec andconstant `Prelude.List.and`
constant
type `List Bool -> Bool`
executable [] := Trueconstant `Prelude.Bool.True`
constructor of datatype `Bool`
type `Bool`
executable
| andconstant `Prelude.List.and`
constant
type `List Bool -> Bool`
executable (Falseconstant `Prelude.Bool.False`
constructor of datatype `Bool`
type `Bool`
executable:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
type in context `Bool -> List Bool -> List Bool`
executable_) := Falseconstant `Prelude.Bool.False`
constructor of datatype `Bool`
type `Bool`
executable
| andconstant `Prelude.List.and`
constant
type `List Bool -> Bool`
executable (Trueconstant `Prelude.Bool.True`
constructor of datatype `Bool`
type `Bool`
executable:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
type in context `Bool -> List Bool -> List Bool`
executablebsvariable `bs`
type `List Bool`) := andconstant `Prelude.List.and` (recursive usage)
constant
type `List Bool -> Bool`
executable bsvariable `bs`
type `List Bool`
declare non-exec andPconstant `Prelude.List.andP`
constant
type `List Prop -> Prop`
non-executable :: [Proptype `Prelude.Bool.Prop`
kind `*`
non-executable] -> Proptype `Prelude.Bool.Prop`
kind `*`
non-executable
define non-exec rec andPconstant `Prelude.List.andP`
constant
type `List Prop -> Prop`
non-executable [] := trueconstant `Prelude.Bool.true`
constant
type `Prop`
non-executable
| andPconstant `Prelude.List.andP`
constant
type `List Prop -> Prop`
non-executable (pvariable `p`
type `Prop`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
type in context `Prop -> List Prop -> List Prop`
executablepsvariable `ps`
type `List Prop`) := pvariable `p`
type `Prop` /\constant `Prelude.Bool.(/\)`
constant
type `Prop -> Prop -> Prop`
non-executable andPconstant `Prelude.List.andP` (recursive usage)
constant
type `List Prop -> Prop`
non-executable psvariable `ps`
type `List Prop`
declare orconstant `Prelude.List.or`
constant
type `List Bool -> Bool`
executable :: [Booldatatype `Prelude.Bool.Bool`
kind `*`
executable] -> Booldatatype `Prelude.Bool.Bool`
kind `*`
executable
define rec orconstant `Prelude.List.or`
constant
type `List Bool -> Bool`
executable [] := Falseconstant `Prelude.Bool.False`
constructor of datatype `Bool`
type `Bool`
executable
| orconstant `Prelude.List.or`
constant
type `List Bool -> Bool`
executable (Trueconstant `Prelude.Bool.True`
constructor of datatype `Bool`
type `Bool`
executable:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
type in context `Bool -> List Bool -> List Bool`
executable_) := Trueconstant `Prelude.Bool.True`
constructor of datatype `Bool`
type `Bool`
executable
| orconstant `Prelude.List.or`
constant
type `List Bool -> Bool`
executable (Falseconstant `Prelude.Bool.False`
constructor of datatype `Bool`
type `Bool`
executable:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
type in context `Bool -> List Bool -> List Bool`
executablebsvariable `bs`
type `List Bool`) := orconstant `Prelude.List.or` (recursive usage)
constant
type `List Bool -> Bool`
executable bsvariable `bs`
type `List Bool`
declare non-exec orPconstant `Prelude.List.orP`
constant
type `List Prop -> Prop`
non-executable :: [Proptype `Prelude.Bool.Prop`
kind `*`
non-executable] -> Proptype `Prelude.Bool.Prop`
kind `*`
non-executable
define non-exec rec orPconstant `Prelude.List.orP`
constant
type `List Prop -> Prop`
non-executable [] := falseconstant `Prelude.Bool.false`
constant
type `Prop`
non-executable
| orPconstant `Prelude.List.orP`
constant
type `List Prop -> Prop`
non-executable (pvariable `p`
type `Prop`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
type in context `Prop -> List Prop -> List Prop`
executablepsvariable `ps`
type `List Prop`) := pvariable `p`
type `Prop` \/constant `Prelude.Bool.(\/)`
constant
type `Prop -> Prop -> Prop`
non-executable orPconstant `Prelude.List.orP` (recursive usage)
constant
type `List Prop -> Prop`
non-executable psvariable `ps`
type `List Prop`
declare allconstant `Prelude.List.all`
constant
type `('a -> Bool) -> List 'a -> Bool`
executable :: ('atype-variable `'a`
kind `*` -> Booldatatype `Prelude.Bool.Bool`
kind `*`
executable) -> ['atype-variable `'a`
kind `*`] -> Booldatatype `Prelude.Bool.Bool`
kind `*`
executable
define rec allconstant `Prelude.List.all`
constant
type `('a -> Bool) -> List 'a -> Bool`
executable _ [] := Trueconstant `Prelude.Bool.True`
constructor of datatype `Bool`
type `Bool`
executable
| allconstant `Prelude.List.all`
constant
type `('a -> Bool) -> List 'a -> Bool`
executable fvariable `f`
type `'a -> Bool` (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executablexsvariable `xs`
type `List 'a`) := if (fvariable `f`
type `'a -> Bool` xvariable `x`
type `'a`) then allconstant `Prelude.List.all` (recursive usage)
constant
type `('a -> Bool) -> List 'a -> Bool`
executable fvariable `f`
type `'a -> Bool` xsvariable `xs`
type `List 'a` else Falseconstant `Prelude.Bool.False`
constructor of datatype `Bool`
type `Bool`
executable
declare anyconstant `Prelude.List.any`
constant
type `('a -> Bool) -> List 'a -> Bool`
executable :: ('atype-variable `'a`
kind `*` -> Booldatatype `Prelude.Bool.Bool`
kind `*`
executable) -> ['atype-variable `'a`
kind `*`] -> Booldatatype `Prelude.Bool.Bool`
kind `*`
executable
define rec anyconstant `Prelude.List.any`
constant
type `('a -> Bool) -> List 'a -> Bool`
executable _ [] := Falseconstant `Prelude.Bool.False`
constructor of datatype `Bool`
type `Bool`
executable
| anyconstant `Prelude.List.any`
constant
type `('a -> Bool) -> List 'a -> Bool`
executable fvariable `f`
type `'a -> Bool` (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executablexsvariable `xs`
type `List 'a`) := if (fvariable `f`
type `'a -> Bool` xvariable `x`
type `'a`) then Trueconstant `Prelude.Bool.True`
constructor of datatype `Bool`
type `Bool`
executable else anyconstant `Prelude.List.any` (recursive usage)
constant
type `('a -> Bool) -> List 'a -> Bool`
executable fvariable `f`
type `'a -> Bool` xsvariable `xs`
type `List 'a`
declare non-exec allPconstant `Prelude.List.allP`
constant
type `('a -> Prop) -> List 'a -> Prop`
non-executable :: ('atype-variable `'a`
kind `*` -> Proptype `Prelude.Bool.Prop`
kind `*`
non-executable) -> ['atype-variable `'a`
kind `*`] -> Proptype `Prelude.Bool.Prop`
kind `*`
non-executable
define non-exec rec allPconstant `Prelude.List.allP`
constant
type `('a -> Prop) -> List 'a -> Prop`
non-executable _ [] := trueconstant `Prelude.Bool.true`
constant
type `Prop`
non-executable
| allPconstant `Prelude.List.allP`
constant
type `('a -> Prop) -> List 'a -> Prop`
non-executable fvariable `f`
type `'a -> Prop` (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executablexsvariable `xs`
type `List 'a`) := (fvariable `f`
type `'a -> Prop` xvariable `x`
type `'a`) /\constant `Prelude.Bool.(/\)`
constant
type `Prop -> Prop -> Prop`
non-executable allPconstant `Prelude.List.allP` (recursive usage)
constant
type `('a -> Prop) -> List 'a -> Prop`
non-executable fvariable `f`
type `'a -> Prop` xsvariable `xs`
type `List 'a`
declare non-exec anyPconstant `Prelude.List.anyP`
constant
type `('a -> Prop) -> List 'a -> Prop`
non-executable :: ('atype-variable `'a`
kind `*` -> Proptype `Prelude.Bool.Prop`
kind `*`
non-executable) -> ['atype-variable `'a`
kind `*`] -> Proptype `Prelude.Bool.Prop`
kind `*`
non-executable
define non-exec rec anyPconstant `Prelude.List.anyP`
constant
type `('a -> Prop) -> List 'a -> Prop`
non-executable _ [] := falseconstant `Prelude.Bool.false`
constant
type `Prop`
non-executable
| anyPconstant `Prelude.List.anyP`
constant
type `('a -> Prop) -> List 'a -> Prop`
non-executable fvariable `f`
type `'a -> Prop` (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executablexsvariable `xs`
type `List 'a`) := (fvariable `f`
type `'a -> Prop` xvariable `x`
type `'a`) \/constant `Prelude.Bool.(\/)`
constant
type `Prop -> Prop -> Prop`
non-executable anyPconstant `Prelude.List.anyP` (recursive usage)
constant
type `('a -> Prop) -> List 'a -> Prop`
non-executable fvariable `f`
type `'a -> Prop` xsvariable `xs`
type `List 'a`
declare elemconstant `Prelude.List.elem`
constant
type `Eq 'a => 'a -> List 'a -> Bool`
executable :: Eqtype-class `Prelude.Eq.Eq`
arguments: ('a :: *)
super-class constraints:
- Prelude.Eq.EqP 'a
has default derive templates 'atype-variable `'a`
kind `*` => 'atype-variable `'a`
kind `*` -> ['atype-variable `'a`
kind `*`] -> Booldatatype `Prelude.Bool.Bool`
kind `*`
executable
define elemconstant `Prelude.List.elem`
constant
type `Eq 'a => 'a -> List 'a -> Bool`
executable xvariable `x`
type `'a` := anyconstant `Prelude.List.any`
constant
type `('a -> Bool) -> List 'a -> Bool`
executable ((==)constant `Prelude.Eq.(==)`
constant of type-class `Eq`
type `'a -> 'a -> Bool`
executable
type-class instance from argument xvariable `x`
type `'a`)
declare notElemconstant `Prelude.List.notElem`
constant
type `Eq 'a => 'a -> List 'a -> Bool`
executable :: Eqtype-class `Prelude.Eq.Eq`
arguments: ('a :: *)
super-class constraints:
- Prelude.Eq.EqP 'a
has default derive templates 'atype-variable `'a`
kind `*` => 'atype-variable `'a`
kind `*` -> ['atype-variable `'a`
kind `*`] -> Booldatatype `Prelude.Bool.Bool`
kind `*`
executable
define notElemconstant `Prelude.List.notElem`
constant
type `Eq 'a => 'a -> List 'a -> Bool`
executable xvariable `x`
type `'a` xsvariable `xs`
type `List 'a` := notconstant `Prelude.Bool.not`
constant
type `Bool -> Bool`
executable (elemconstant `Prelude.List.elem`
constant
type `Eq 'a => 'a -> List 'a -> Bool`
type in context `'a -> List 'a -> Bool`
executable xvariable `x`
type `'a` xsvariable `xs`
type `List 'a`)
{-# inline notElemconstant `Prelude.List.notElem`
constant
type `Eq 'a => 'a -> List 'a -> Bool`
executable #-}
declare non-exec elemPconstant `Prelude.List.elemP`
constant
type `EqP 'a => 'a -> List 'a -> Prop`
non-executable :: EqPtype-class `Prelude.Eq.EqP`
arguments: ('a :: *)
has default derive templates
derive-template labels
- eq (only deriving)
- full 'atype-variable `'a`
kind `*` => 'atype-variable `'a`
kind `*` -> ['atype-variable `'a`
kind `*`] -> Proptype `Prelude.Bool.Prop`
kind `*`
non-executable
define non-exec elemPconstant `Prelude.List.elemP`
constant
type `EqP 'a => 'a -> List 'a -> Prop`
non-executable xvariable `x`
type `'a` := anyPconstant `Prelude.List.anyP`
constant
type `('a -> Prop) -> List 'a -> Prop`
non-executable ((===)constant `Prelude.Eq.(===)`
constant of type-class `EqP`
type `'a -> 'a -> Prop`
non-executable
type-class instance from argument xvariable `x`
type `'a`)
declare non-exec notElemPconstant `Prelude.List.notElemP`
constant
type `EqP 'a => 'a -> List 'a -> Prop`
non-executable :: EqPtype-class `Prelude.Eq.EqP`
arguments: ('a :: *)
has default derive templates
derive-template labels
- eq (only deriving)
- full 'atype-variable `'a`
kind `*` => 'atype-variable `'a`
kind `*` -> ['atype-variable `'a`
kind `*`] -> Proptype `Prelude.Bool.Prop`
kind `*`
non-executable
define non-exec notElemPconstant `Prelude.List.notElemP`
constant
type `EqP 'a => 'a -> List 'a -> Prop`
non-executable xvariable `x`
type `'a` xsvariable `xs`
type `List 'a` := notPconstant `Prelude.Bool.notP`
constant
type `Prop -> Prop`
non-executable (elemPconstant `Prelude.List.elemP`
constant
type `EqP 'a => 'a -> List 'a -> Prop`
type in context `'a -> List 'a -> Prop`
non-executable xvariable `x`
type `'a` xsvariable `xs`
type `List 'a`)
{-# inline notElemPconstant `Prelude.List.notElemP`
constant
type `EqP 'a => 'a -> List 'a -> Prop`
non-executable #-}
derive Listdatatype `Prelude.List.List`
kind `* -> *`
executable instances (Eqtype-class `Prelude.Eq.Eq`
arguments: ('a :: *)
super-class constraints:
- Prelude.Eq.EqP 'a
has default derive templates
generated code:
instance Eq 'a => Eq (List 'a) where
define rec (==) Nil Nil := True
| (==) ((:) x1 x2) ((:) y1 y2) := (x1 == y1) && (x2 == y2)
| (==) _ _ := False
end-instance
, EqPtype-class `Prelude.Eq.EqP`
arguments: ('a :: *)
has default derive templates
derive-template labels
- eq (only deriving)
- full
generated code:
instance EqP 'a => EqP (List 'a) where
define non-exec rec (===) Nil Nil := true
| (===) ((:) x1 x2) ((:) y1 y2) := (x1 === y1) /\ (x2 === y2)
| (===) _ _ := false
end-instance
, Ordtype-class `Prelude.Ord.Ord`
arguments: ('a :: *)
super-class constraints:
- Prelude.Eq.Eq 'a
has default derive templates
generated code:
instance Ord 'a => Ord (List 'a) where
define rec compare Nil Nil := EQ
| compare Nil _ := LT
| compare _ Nil := GT
| compare ((:) x1 x2) ((:) y1 y2) := lexCompare x1 y1 $ compare x2 y2
end-instance
)
declare nubByconstant `Prelude.List.nubBy`
constant
type `('a -> 'a -> Bool) -> List 'a -> List 'a`
executable :: ('atype-variable `'a`
kind `*` -> 'atype-variable `'a`
kind `*` -> Booldatatype `Prelude.Bool.Bool`
kind `*`
executable) -> ['atype-variable `'a`
kind `*`] -> ['atype-variable `'a`
kind `*`]
define rec nubByconstant `Prelude.List.nubBy`
constant
type `('a -> 'a -> Bool) -> List 'a -> List 'a`
executable _ [] := []
| nubByconstant `Prelude.List.nubBy`
constant
type `('a -> 'a -> Bool) -> List 'a -> List 'a`
executable pvariable `p`
type `'a -> 'a -> Bool` (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executablexsvariable `xs`
type `List 'a`) := xvariable `x`
type `'a` :constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> List 'a -> List 'a`
executable nubByconstant `Prelude.List.nubBy` (recursive usage)
constant
type `('a -> 'a -> Bool) -> List 'a -> List 'a`
executable pvariable `p`
type `'a -> 'a -> Bool` (filterconstant `Prelude.List.filter`
constant
type `('a -> Bool) -> List 'a -> List 'a`
executable (fntype `'a -> Bool` yvariable `y`
type `'a` -> notconstant `Prelude.Bool.not`
constant
type `Bool -> Bool`
executable (pvariable `p`
type `'a -> 'a -> Bool` xvariable `x`
type `'a` yvariable `y`
type `'a`)) xsvariable `xs`
type `List 'a`)
declare nubconstant `Prelude.List.nub`
constant
type `Eq 'a => List 'a -> List 'a`
executable :: Eqtype-class `Prelude.Eq.Eq`
arguments: ('a :: *)
super-class constraints:
- Prelude.Eq.EqP 'a
has default derive templates 'atype-variable `'a`
kind `*` => ['atype-variable `'a`
kind `*`] -> ['atype-variable `'a`
kind `*`]
define nubconstant `Prelude.List.nub`
constant
type `Eq 'a => List 'a -> List 'a`
executable := nubByconstant `Prelude.List.nubBy`
constant
type `('a -> 'a -> Bool) -> List 'a -> List 'a`
executable (==)constant `Prelude.Eq.(==)`
constant of type-class `Eq`
type `'a -> 'a -> Bool`
executable
type-class instance from argument
{-# inline nubconstant `Prelude.List.nub`
constant
type `Eq 'a => List 'a -> List 'a`
executable #-}
end-moduleend of module Prelude.List
|