From 399e30f085df96e11f12fed4c879c3ad661c39c5 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 9 Jan 2021 21:31:07 -0800
Subject: [PATCH] Solve homework one and two

---
 HomeworkOne.idr | 24 ++++++++++++++++++++++++
 HomeworkTwo.idr | 21 +++++++++++++++++++++
 2 files changed, 45 insertions(+)
 create mode 100644 HomeworkOne.idr
 create mode 100644 HomeworkTwo.idr

diff --git a/HomeworkOne.idr b/HomeworkOne.idr
new file mode 100644
index 0000000..9ff85ad
--- /dev/null
+++ b/HomeworkOne.idr
@@ -0,0 +1,24 @@
+module HomeworkOne
+import Data.Fin
+
+%default total
+
+Tuple : Nat -> Type
+Tuple Z = Nat
+Tuple (S n) = (Nat, Tuple n)
+
+first : { s : Nat } -> Tuple s -> Nat
+first {s=Z} n = n
+first {s=S n} (f, r) = f
+
+lst : { s : Nat } -> Tuple s -> Nat
+lst {s=Z} n = n
+lst {s=S n} (f, r) = lst r
+
+-- Yeah, yeah, this isn't as specified in the
+-- homework assingment. But what do you want
+-- us to do with the "zero" case or the "past the edge" case?
+-- Return 0? Not pretty.
+project : Fin (S k) -> Tuple k -> Nat
+project FZ t = first t
+project {k=S _} (FS n) (f, r) = project n r
diff --git a/HomeworkTwo.idr b/HomeworkTwo.idr
new file mode 100644
index 0000000..032b6e9
--- /dev/null
+++ b/HomeworkTwo.idr
@@ -0,0 +1,21 @@
+module HomeworkOne
+import Data.Vect
+
+%default total
+
+zipW : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
+zipW _ [] [] = []
+zipW f (x::xs) (y::ys) = f x y :: zipWith f xs ys 
+
+lst : Vect (S n) a -> a
+lst (x::[]) = x 
+lst (_::x::xs) = lst (x::xs)
+
+initial : Vect (S n) a -> Vect n a
+initial (x::[]) = []
+initial (x1::x2::xs) = x1 :: initial (x2::xs)
+
+palin : Eq a => Vect n a -> Bool
+palin [] = True
+palin [x] = True
+palin (x1::l@(x2::xs)) = x1 == lst l && (palin $ initial l)