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
|
let PList =
http://prelude.dhall-lang.org/List/package.dhall sha256:ca82b0e91b63a044b425b47a0ac02c3c0e726acf1c8b567cdc24ebac0073209a
let tail
: forall(a: Type)
-> List a
-> List a
= \(a: Type)
-> \(l: List a)
-> List/Build
a
( λ(list : Type)
→ λ(cons : a → list → list)
→ λ(nil : list)
→ List/fold a l list (
\(x: a) ->
\(p: list) ->
nil
) nil
)
List/fold
a
l
(List a)
( \(x: a)
-> \(q: List a)
-> q
)
([] : List a)
in tail Text [ "ABC", "DEF", "GHI" ]
-- let nth
-- : forall(a : Type)
-- -> Natural
-- -> List a
-- -> Optional a
-- = \(a: Type)
-- -> \(n: Natural)
-- -> \(l: List a)
-- -> Natural/fold n
--
-- in nth Text 2 [ "ABC", "DEF", "GHI" ]
-- let zip
-- : ∀(a : Type)
-- → ∀(b : Type)
-- → { _1 : List a, _2 : List b }
-- → List { _1 : a, _2 : b }
-- = λ(a : Type)
-- → λ(b : Type)
-- → λ(xs : { _1 : List a, _2 : List b })
-- -- → List/build
-- -- { _1 : a, _2 : b }
-- -- ( λ(list : Type)
-- -- → λ(cons : { _1 : a, _2 : b } → list → list)
-- -- → λ(nil : list)
-- -- → List/fold { index : Natural, value : a } (List/indexed a xs._1) list (
-- -- \(x: { index : Natural, value : a }) ->
-- -- \(p: list) ->
-- -- List/fold b xs._2 list (\(y: b) -> \(q: list) -> cons { _1 = x.value, _2 = y } q) nil : list
-- -- ) nil
-- -- )
-- → PList.map { index : Natural, value : a } { index : Natural, value : a } (List/indexed a xs._1) (
-- \(x: { index : Natural, value : a }) ->
-- List/fold b xs._2 list (\(y: b) -> \(q: list) -> cons { _1 = x.value, _2 = y } q) nil : list
-- ) nil
--
-- in zip Text Bool { _1 = [ "ABC", "DEF", "GHI" ], _2 = [ True, False, True ] }
|
