25 lines
561 B
Idris
25 lines
561 B
Idris
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
|