Htaut.Proving

Documentation

data Prove a

Constructors

Evidence a

Instances

Monad Prove

Methods

(>>=) :: Prove a -> (a -> Prove b) -> Prove b

(>>) :: Prove a -> Prove b -> Prove b

return :: a -> Prove a

fail :: String -> Prove a

Functor Prove

Methods

fmap :: (a -> b) -> Prove a -> Prove b

(<$) :: a -> Prove b -> Prove a

Applicative Prove

Methods

pure :: a -> Prove a

(<*>) :: Prove (a -> b) -> Prove a -> Prove b

(*>) :: Prove a -> Prove b -> Prove b

(<*) :: Prove a -> Prove b -> Prove a

exfalso :: Prop a => Prove (Bottom -> a)