basic mathematical logic in Idris

Logic.idr

module Logic

infixr 1 ==>

(==>) : Bool -> Bool -> Bool
False ==> _ = True
True  ==> x = x

data Exists : (A : Type) -> (P : A -> Bool) -> Type where
  exists : {A : Type} -> {P : A -> Bool} -> (a : A) -> so (P a) -> Exists A P

prop : Exists Integer (\n => n > 0)
prop = exists 2 oh

prop' : Exists Integer (\n => (n == 2) ==> (n /= 3))
prop' = exists 2 oh