summaryrefslogtreecommitdiff
path: root/test.dhall
diff options
context:
space:
mode:
Diffstat (limited to 'test.dhall')
-rw-r--r--test.dhall68
1 files changed, 68 insertions, 0 deletions
diff --git a/test.dhall b/test.dhall
new file mode 100644
index 0000000..5bc4c88
--- /dev/null
+++ b/test.dhall
@@ -0,0 +1,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 ] }