gistfile1.txt

module ExerciseSeven where

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + n = n
(succ m) + n = succ (m + n)

_×_ : ℕ → ℕ → ℕ
-- Implement here
zero × n = zero
(succ m) × n = n + (m × n)

data Maybe (A : Set) : Set where
  Nothing : Maybe A
  Just : A -> Maybe A

pred : ℕ → Maybe ℕ
(pred (succ m)) = (Just m)
(pred zero) = Nothing

data Vec (A : Set) : ℕ → Set where
   [] : Vec A zero
   _∷_ : ∀ {n} → A → Vec A n → Vec A (succ n)

_++_ : ∀ {A}{m n : ℕ} → Vec A m → Vec A n → Vec A (m + n)
[] ++ y = y
(x ∷ xs) ++ y = x ∷ (xs ++ y)

head : ∀{A}{n : ℕ} → Vec A (succ n) → A
(head (x ∷ xs)) = x 

concat : ∀{A}{n m : ℕ} → Vec (Vec A m) n -> Vec A (n × m)
(concat []) = []
(concat (x ∷ xs)) = x ++ (concat xs)