summaryrefslogtreecommitdiff
path: root/test.dhall
diff options
context:
space:
mode:
authorNadrieril2019-12-21 21:32:19 +0000
committerNadrieril2019-12-21 21:32:19 +0000
commitc9f8500cd7463652e7ccc1be59afa29c484037a3 (patch)
treebb3561841ac40cacc41409ac4fd02fbd4a6ac095 /test.dhall
parentfa6bf7e0c8da8172dd7905ba38b72b3a0c74a1ba (diff)
Remove leftover file
Diffstat (limited to 'test.dhall')
-rw-r--r--test.dhall68
1 files changed, 0 insertions, 68 deletions
diff --git a/test.dhall b/test.dhall
deleted file mode 100644
index 5bc4c88..0000000
--- a/test.dhall
+++ /dev/null
@@ -1,68 +0,0 @@
-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 ] }