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