siddhartha-gadgil

moduspoens : {P : Set} → {Q : Set} → P → (P → Q) → Q
moduspoens p imp = imp p

siddhartha-gadgil

data True : Set where
  qed : True


data False : Set where

-- false has no constructors

siddhartha-gadgil

_flatMapOption_ : {A : Set} → {B : Set} → Option A → (A →  Option B) → Option B
None flatMapOption _ = None
(Some a) flatMapOption f = f a

siddhartha-gadgil

_mapOption_ : {A : Set} → {B : Set} → Option A → (A → B) → Option B
None mapOption _ = None
(Some a) mapOption f = Some (f a)

siddhartha-gadgil

_find_ : {A : Set} → List A → (A → Bool) → Option A
[] find _ = None
(x :: xs) find p = if (p x) then (Some x) else (xs find p)

siddhartha-gadgil

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

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

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

_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

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