From c9f8500cd7463652e7ccc1be59afa29c484037a3 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 21 Dec 2019 21:32:19 +0000
Subject: Remove leftover file

---
 test.dhall | 68 --------------------------------------------------------------
 1 file changed, 68 deletions(-)
 delete mode 100644 test.dhall

(limited to 'test.dhall')

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 ] }
-- 
cgit v1.2.3