siddhartha-gadgil

_contains_ : {A : Set} → List A → (A → Bool) → Bool
[] contains _ = false
(x :: xs) contains p = (p x) || (xs contains p)

siddhartha-gadgil

_:+_ : {A : Set} → {n : ℕ} → A → Vec A n → Vec A (succ n)
a :+ [] = a :: []
a :+ (x :: xs) = x :: (a :+ xs)

siddhartha-gadgil

zipop : {A : Set} → {n : ℕ} → Vec A n → Vec A n → (A → A → A) → Vec A n
zipop  [] [] _ = []
zipop  (x :: xs) (y :: ys) op = (op x y) :: (zipop  xs ys op)

siddhartha-gadgil

countdown : (n : ℕ) → Vec ℕ (succ n)
countdown zero = zero :: []
countdown (succ m) = (succ m) :: (countdown m)

siddhartha-gadgil

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

siddhartha-gadgil

_flatMap_ : {A B : Set} → List A → (A → List B) → List B
[] flatMap _ = []
(a :: xs) flatMap f = (f a) ++ (xs flatMap f)

siddhartha-gadgil

_map_ : {A B : Set} → List A → (A → B) → List B
[] map _ = []
(a :: xs) map f = (f a) :: (xs map f)

twothreefour : List ℕ
twothreefour = onetwothree map succ

siddhartha-gadgil

_++_ : {A : Set} → List A → List A → List A
[] ++ l = l
(a :: xs) ++ l = a :: (xs ++ l)

reverse : {A : Set} → List A → List A
reverse [] = []
reverse (a :: l) = (reverse l) ++ (a :: [])

siddhartha-gadgil

length : {A : Set} → List A → ℕ
length [] = zero
length (a :: l) = succ (length l)

siddhartha-gadgil

length₀ : (A : Set) → List A → ℕ
length₀ _ [] = zero
length₀ A (a :: l) = succ (length₀ A l)