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

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

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

data True : Set where
  qed : True


data False : Set where

-- false has no constructors

siddhartha-gadgil

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

siddhartha-gadgil

vacuous : {A : Set} → False → A
vacuous ()

siddhartha-gadgil

data Even : ℕ → Set where
  zeroeven : Even zero
  +2even : {n : ℕ} → Even n → Even (succ (succ n))

siddhartha-gadgil

2even : Even 2
2even = +2even zeroeven

siddhartha-gadgil

1odd : Even 1 → False
1odd ()

siddhartha-gadgil

data _==_ {A : Set} : A → A → Set where
  refl : (a : A) → a == a