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
|
module Data.List (
module Prelude.List,
replicateconstant `Data.List.replicate`
constant
type `Natural -> 'a -> ['a]`
executable,
takeconstant `Data.List.take`
constant
type `Natural -> ['a] -> ['a]`
executable,
dropconstant `Data.List.drop`
constant
type `Natural -> ['a] -> ['a]`
executable,
splitAtconstant `Data.List.splitAt`
constant
type `Natural -> ['a] -> (['a], ['a])`
executable,
takeWhileconstant `Data.List.takeWhile`
constant
type `('a -> Bool) -> ['a] -> ['a]`
executable,
dropWhileconstant `Data.List.dropWhile`
constant
type `('a -> Bool) -> ['a] -> ['a]`
executable,
breakconstant `Data.List.break`
constant
type `('a -> Bool) -> ['a] -> (['a], ['a])`
executable,
spanconstant `Data.List.span`
constant
type `('a -> Bool) -> ['a] -> (['a], ['a])`
executable,
lookupconstant `Data.List.lookup`
constant
type `Eq 'k => 'k -> [('k, 'v)] -> Maybe 'v`
executable,
zipconstant `Data.List.zip`
constant
type `['a] -> ['b] -> [('a, 'b)]`
executable,
unzipconstant `Data.List.unzip`
constant
type `[('a, 'b)] -> (['a], ['b])`
executable
) where
declare replicateconstant `Data.List.replicate`
constant
type `Natural -> 'a -> ['a]`
executable :: Naturaldatatype `Prelude.Num.Natural`
kind `*`
executable -> 'atype-variable `'a`
kind `*` -> ['atype-variable `'a`
kind `*`]
define rec replicateconstant `Data.List.replicate`
constant
type `Natural -> 'a -> ['a]`
executable 0natural number literal
type `Natural`
decimal value: 0
hexadecimal value: 0x0
octal value: 0o0
binary value: 0b0 _ := []
| replicateconstant `Data.List.replicate`
constant
type `Natural -> 'a -> ['a]`
executable nvariable `n`
type `Natural` avariable `a`
type `'a` := avariable `a`
type `'a` :constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> ['a] -> ['a]`
executable (replicateconstant `Data.List.replicate` (recursive usage)
constant
type `Natural -> 'a -> ['a]`
executable (predconstant `Prelude.BasicClasses.pred`
constant of type-class `Enum`
type `'a -> 'a`
type in context `Natural -> Natural`
executable
statically resolved type-class instance nvariable `n`
type `Natural`) avariable `a`
type `'a`)
declare takeconstant `Data.List.take`
constant
type `Natural -> ['a] -> ['a]`
executable :: Naturaldatatype `Prelude.Num.Natural`
kind `*`
executable -> ['atype-variable `'a`
kind `*`] -> ['atype-variable `'a`
kind `*`]
define rec takeconstant `Data.List.take`
constant
type `Natural -> ['a] -> ['a]`
executable 0natural number literal
type `Natural`
decimal value: 0
hexadecimal value: 0x0
octal value: 0o0
binary value: 0b0 _ := []
| takeconstant `Data.List.take`
constant
type `Natural -> ['a] -> ['a]`
executable _ [] := []
| takeconstant `Data.List.take`
constant
type `Natural -> ['a] -> ['a]`
executable nvariable `n`
type `Natural` (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> ['a] -> ['a]`
executablexsvariable `xs`
type `['a]`) := xvariable `x`
type `'a` :constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> ['a] -> ['a]`
executable (takeconstant `Data.List.take` (recursive usage)
constant
type `Natural -> ['a] -> ['a]`
executable (predconstant `Prelude.BasicClasses.pred`
constant of type-class `Enum`
type `'a -> 'a`
type in context `Natural -> Natural`
executable
statically resolved type-class instance nvariable `n`
type `Natural`) xsvariable `xs`
type `['a]`)
declare dropconstant `Data.List.drop`
constant
type `Natural -> ['a] -> ['a]`
executable :: Naturaldatatype `Prelude.Num.Natural`
kind `*`
executable -> ['atype-variable `'a`
kind `*`] -> ['atype-variable `'a`
kind `*`]
define rec dropconstant `Data.List.drop`
constant
type `Natural -> ['a] -> ['a]`
executable 0natural number literal
type `Natural`
decimal value: 0
hexadecimal value: 0x0
octal value: 0o0
binary value: 0b0 lvariable `l`
type `['a]` := lvariable `l`
type `['a]`
| dropconstant `Data.List.drop`
constant
type `Natural -> ['a] -> ['a]`
executable _ [] := []
| dropconstant `Data.List.drop`
constant
type `Natural -> ['a] -> ['a]`
executable nvariable `n`
type `Natural` (_:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> ['a] -> ['a]`
executablexsvariable `xs`
type `['a]`) := dropconstant `Data.List.drop` (recursive usage)
constant
type `Natural -> ['a] -> ['a]`
executable (predconstant `Prelude.BasicClasses.pred`
constant of type-class `Enum`
type `'a -> 'a`
type in context `Natural -> Natural`
executable
statically resolved type-class instance nvariable `n`
type `Natural`) xsvariable `xs`
type `['a]`
declare splitAtconstant `Data.List.splitAt`
constant
type `Natural -> ['a] -> (['a], ['a])`
executable :: Naturaldatatype `Prelude.Num.Natural`
kind `*`
executable -> ['atype-variable `'a`
kind `*`] -> (['atype-variable `'a`
kind `*`], ['atype-variable `'a`
kind `*`])
define rec splitAtconstant `Data.List.splitAt`
constant
type `Natural -> ['a] -> (['a], ['a])`
executable 0natural number literal
type `Natural`
decimal value: 0
hexadecimal value: 0x0
octal value: 0o0
binary value: 0b0 lvariable `l`
type `['a]` := ([], lvariable `l`
type `['a]`)
| splitAtconstant `Data.List.splitAt`
constant
type `Natural -> ['a] -> (['a], ['a])`
executable _ [] := ([], [])
| splitAtconstant `Data.List.splitAt`
constant
type `Natural -> ['a] -> (['a], ['a])`
executable nvariable `n`
type `Natural` (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> ['a] -> ['a]`
executablexsvariable `xs`
type `['a]`) :=
let
val (ltvariable `lt`
type `['a]`, ldvariable `ld`
type `['a]`) = (splitAtconstant `Data.List.splitAt` (recursive usage)
constant
type `Natural -> ['a] -> (['a], ['a])`
executable (predconstant `Prelude.BasicClasses.pred`
constant of type-class `Enum`
type `'a -> 'a`
type in context `Natural -> Natural`
executable
statically resolved type-class instance nvariable `n`
type `Natural`) xsvariable `xs`
type `['a]`)
in
(xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> ['a] -> ['a]`
executableltvariable `lt`
type `['a]`, ldvariable `ld`
type `['a]`)
end
property EqPtype-class `Prelude.Eq.EqP`
arguments: ('a :: *)
has default derive templates
derive-template labels
- eq (only deriving)
- full 'atype-variable `'a`
kind `*` => splitAt_take_dropconstant `Data.List.splitAt_take_drop`
property
type `EqP 'a => Natural -> ['a] -> Prop`
non-executable nvariable `n`
type `Natural` (lvariable `l`
type `['a]` :: ['atype-variable `'a`
kind `*`]) := ((splitAtconstant `Data.List.splitAt`
constant
type `Natural -> ['a] -> (['a], ['a])`
executable nvariable `n`
type `Natural` lvariable `l`
type `['a]`) ===constant `Prelude.Eq.(===)`
constant of type-class `EqP`
type `'a -> 'a -> Prop`
type in context `(['a], ['a]) -> (['a], ['a]) -> Prop`
non-executable
statically resolved type-class instance (takeconstant `Data.List.take`
constant
type `Natural -> ['a] -> ['a]`
executable nvariable `n`
type `Natural` lvariable `l`
type `['a]`, dropconstant `Data.List.drop`
constant
type `Natural -> ['a] -> ['a]`
executable nvariable `n`
type `Natural` lvariable `l`
type `['a]`))
declare takeWhileconstant `Data.List.takeWhile`
constant
type `('a -> Bool) -> ['a] -> ['a]`
executable :: ('atype-variable `'a`
kind `*` -> Booldatatype `Prelude.Bool.Bool`
kind `*`
executable) -> ['atype-variable `'a`
kind `*`] -> ['atype-variable `'a`
kind `*`]
define rec takeWhileconstant `Data.List.takeWhile`
constant
type `('a -> Bool) -> ['a] -> ['a]`
executable _ [] := []
| takeWhileconstant `Data.List.takeWhile`
constant
type `('a -> Bool) -> ['a] -> ['a]`
executable pvariable `p`
type `'a -> Bool` (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> ['a] -> ['a]`
executablexsvariable `xs`
type `['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 -> ['a] -> ['a]`
executable (takeWhileconstant `Data.List.takeWhile` (recursive usage)
constant
type `('a -> Bool) -> ['a] -> ['a]`
executable pvariable `p`
type `'a -> Bool` xsvariable `xs`
type `['a]`) else []
declare dropWhileconstant `Data.List.dropWhile`
constant
type `('a -> Bool) -> ['a] -> ['a]`
executable :: ('atype-variable `'a`
kind `*` -> Booldatatype `Prelude.Bool.Bool`
kind `*`
executable) -> ['atype-variable `'a`
kind `*`] -> ['atype-variable `'a`
kind `*`]
define rec dropWhileconstant `Data.List.dropWhile`
constant
type `('a -> Bool) -> ['a] -> ['a]`
executable _ [] := []
| dropWhileconstant `Data.List.dropWhile`
constant
type `('a -> Bool) -> ['a] -> ['a]`
executable pvariable `p`
type `'a -> Bool` (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> ['a] -> ['a]`
executablexsvariable `xs`
type `['a]`) :=
if (pvariable `p`
type `'a -> Bool` xvariable `x`
type `'a`) then (dropWhileconstant `Data.List.dropWhile` (recursive usage)
constant
type `('a -> Bool) -> ['a] -> ['a]`
executable pvariable `p`
type `'a -> Bool` xsvariable `xs`
type `['a]`) else (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> ['a] -> ['a]`
executablexsvariable `xs`
type `['a]`)
declare spanconstant `Data.List.span`
constant
type `('a -> Bool) -> ['a] -> (['a], ['a])`
executable :: ('atype-variable `'a`
kind `*` -> Booldatatype `Prelude.Bool.Bool`
kind `*`
executable) -> ['atype-variable `'a`
kind `*`] -> (['atype-variable `'a`
kind `*`], ['atype-variable `'a`
kind `*`])
define rec spanconstant `Data.List.span`
constant
type `('a -> Bool) -> ['a] -> (['a], ['a])`
executable _ [] := ([], [])
| spanconstant `Data.List.span`
constant
type `('a -> Bool) -> ['a] -> (['a], ['a])`
executable pvariable `p`
type `'a -> Bool` (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> ['a] -> ['a]`
executablexsvariable `xs`
type `['a]`) :=
if (pvariable `p`
type `'a -> Bool` xvariable `x`
type `'a`) then
let val (ysvariable `ys`
type `['a]`, zsvariable `zs`
type `['a]`) = spanconstant `Data.List.span` (recursive usage)
constant
type `('a -> Bool) -> ['a] -> (['a], ['a])`
executable pvariable `p`
type `'a -> Bool` xsvariable `xs`
type `['a]` in
(xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> ['a] -> ['a]`
executableysvariable `ys`
type `['a]`, zsvariable `zs`
type `['a]`)
end
else ([], xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> ['a] -> ['a]`
executablexsvariable `xs`
type `['a]`)
declare breakconstant `Data.List.break`
constant
type `('a -> Bool) -> ['a] -> (['a], ['a])`
executable :: ('atype-variable `'a`
kind `*` -> Booldatatype `Prelude.Bool.Bool`
kind `*`
executable) -> ['atype-variable `'a`
kind `*`] -> (['atype-variable `'a`
kind `*`], ['atype-variable `'a`
kind `*`])
define breakconstant `Data.List.break`
constant
type `('a -> Bool) -> ['a] -> (['a], ['a])`
executable pvariable `p`
type `'a -> Bool` := spanconstant `Data.List.span`
constant
type `('a -> Bool) -> ['a] -> (['a], ['a])`
executable (notconstant `Prelude.Bool.not`
constant
type `Bool -> Bool`
executable .constant `Prelude.Function.(.)`
constant of type-class `Dot`
type `'a -> 'b -> 'c`
type in context `(Bool -> Bool) -> ('a -> Bool) -> 'a -> Bool`
executable
statically resolved type-class instance pvariable `p`
type `'a -> Bool`)
declare lookupconstant `Data.List.lookup`
constant
type `Eq 'k => 'k -> [('k, 'v)] -> Maybe 'v`
executable :: Eqtype-class `Prelude.Eq.Eq`
arguments: ('a :: *)
super-class constraints:
- Prelude.Eq.EqP 'a
has default derive templates 'ktype-variable `'k`
kind `*` => 'ktype-variable `'k`
kind `*` -> [('ktype-variable `'k`
kind `*`, 'vtype-variable `'v`
kind `*`)] -> Maybedatatype `Prelude.Maybe.Maybe`
kind `* -> *`
executable 'vtype-variable `'v`
kind `*`
define rec lookupconstant `Data.List.lookup`
constant
type `Eq 'k => 'k -> [('k, 'v)] -> Maybe 'v`
executable _keyvariable `_key`
type `'k` [] := Nothingconstant `Prelude.Maybe.Nothing`
constructor of datatype `Maybe`
type `Maybe 'a`
type in context `Maybe 'v`
executable
| lookupconstant `Data.List.lookup`
constant
type `Eq 'k => 'k -> [('k, 'v)] -> Maybe 'v`
executable keyvariable `key`
type `'k` ((kvariable `k`
type `'k`, vvariable `v`
type `'v`):constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> ['a] -> ['a]`
type in context `('k, 'v) -> [('k, 'v)] -> [('k, 'v)]`
executablekvsvariable `kvs`
type `[('k, 'v)]`) :=
if (keyvariable `key`
type `'k` ==constant `Prelude.Eq.(==)`
constant of type-class `Eq`
type `'a -> 'a -> Bool`
type in context `'k -> 'k -> Bool`
executable
type-class instance from argument kvariable `k`
type `'k`) then Justconstant `Prelude.Maybe.Just`
constructor of datatype `Maybe`
type `'a -> Maybe 'a`
type in context `'v -> Maybe 'v`
executable vvariable `v`
type `'v` else lookupconstant `Data.List.lookup` (recursive usage)
constant
type `Eq 'k => 'k -> [('k, 'v)] -> Maybe 'v`
executable keyvariable `key`
type `'k` kvsvariable `kvs`
type `[('k, 'v)]`
declare zipWithconstant `Data.List.zipWith`
constant
type `('a -> 'b -> 'c) -> ['a] -> ['b] -> ['c]`
executable :: ('atype-variable `'a`
kind `*` -> 'btype-variable `'b`
kind `*` -> 'ctype-variable `'c`
kind `*`) -> ['atype-variable `'a`
kind `*`] -> ['btype-variable `'b`
kind `*`] -> ['ctype-variable `'c`
kind `*`]
define rec zipWithconstant `Data.List.zipWith`
constant
type `('a -> 'b -> 'c) -> ['a] -> ['b] -> ['c]`
executable fvariable `f`
type `'a -> 'b -> 'c` (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> ['a] -> ['a]`
executablexsvariable `xs`
type `['a]`) (yvariable `y`
type `'b`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> ['a] -> ['a]`
type in context `'b -> ['b] -> ['b]`
executableysvariable `ys`
type `['b]`) := (fvariable `f`
type `'a -> 'b -> 'c` xvariable `x`
type `'a` yvariable `y`
type `'b`):constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> ['a] -> ['a]`
type in context `'c -> ['c] -> ['c]`
executable(zipWithconstant `Data.List.zipWith` (recursive usage)
constant
type `('a -> 'b -> 'c) -> ['a] -> ['b] -> ['c]`
executable fvariable `f`
type `'a -> 'b -> 'c` xsvariable `xs`
type `['a]` ysvariable `ys`
type `['b]`)
| zipWithconstant `Data.List.zipWith`
constant
type `('a -> 'b -> 'c) -> ['a] -> ['b] -> ['c]`
executable _ _ _ := undefinedconstant `Prelude.Default.undefined`
constant of type-class `Default`
type `'a`
type in context `['c]`
executable
statically resolved type-class instance
declare zipconstant `Data.List.zip`
constant
type `['a] -> ['b] -> [('a, 'b)]`
executable :: ['atype-variable `'a`
kind `*`] -> ['btype-variable `'b`
kind `*`] -> [('atype-variable `'a`
kind `*`, 'btype-variable `'b`
kind `*`)]
define zipconstant `Data.List.zip`
constant
type `['a] -> ['b] -> [('a, 'b)]`
executable := zipWithconstant `Data.List.zipWith`
constant
type `('a -> 'b -> 'c) -> ['a] -> ['b] -> ['c]`
type in context `('a -> 'b -> ('a, 'b)) -> ['a] -> ['b] -> [('a, 'b)]`
executable (fntype `'a -> 'b -> ('a, 'b)` xvariable `x`
type `'a` yvariable `y`
type `'b` -> (xvariable `x`
type `'a`, yvariable `y`
type `'b`))
declare unzipconstant `Data.List.unzip`
constant
type `[('a, 'b)] -> (['a], ['b])`
executable :: [('atype-variable `'a`
kind `*`,'btype-variable `'b`
kind `*`)] -> (['atype-variable `'a`
kind `*`],['btype-variable `'b`
kind `*`])
define unzipconstant `Data.List.unzip`
constant
type `[('a, 'b)] -> (['a], ['b])`
executable := foldrconstant `Prelude.Foldable.foldr`
statically resolved constant of type-class `Foldable`
type `('e -> 'acc -> 'acc) -> 'acc -> 't -> 'acc`
type in context `(('a, 'b) -> (['a], ['b]) -> (['a], ['b])) -> (['a], ['b]) -> [('a, 'b)] -> (['a], ['b])`
executable
statically resolved type-class instance (fntype `('a, 'b) -> (['a], ['b]) -> (['a], ['b])` (xvariable `x`
type `'a`,yvariable `y`
type `'b`) (xsvariable `xs`
type `['a]`,ysvariable `ys`
type `['b]`) -> (xvariable `x`
type `'a`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> ['a] -> ['a]`
executablexsvariable `xs`
type `['a]`,yvariable `y`
type `'b`:constant `Prelude.List.(:)`
constructor of datatype `List`
type `'a -> ['a] -> ['a]`
type in context `'b -> ['b] -> ['b]`
executableysvariable `ys`
type `['b]`)) ([],[])
end-moduleend of module Data.List
|