siddhartha-gadgil

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

siddhartha-gadgil

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

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

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

siddhartha-gadgil

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

siddhartha-gadgil

if_then_else : {A : Set} → Bool → A → A  → A
if true then x else _ = x
if false then _ else y = y

siddhartha-gadgil

_filter_ : {A : Set} → List A → (A → Bool) → List A
[] filter _ = []
(x :: xs) filter p = if (p x) then (x :: (xs filter p)) else (xs filter p)

siddhartha-gadgil

fold_by_from_ : {A : Set} → {B : Set} → List A → (A → B → B) → B → B
fold [] by _ from b = b
fold (x :: xs) by op from b = op x (fold xs by op from b)

siddhartha-gadgil

open import Nat

upto : ℕ → List ℕ
upto zero = []
upto (succ n) = (upto n) ++ ((succ n) :: [])

listsqs : ℕ → List ℕ
listsqs n = upto n map (λ x → (x * x))

sumsqs : ℕ → ℕ

siddhartha-gadgil

data Option (A : Set) : Set where
  Some : A → Option A
  None : Option A