g4ip-prover-2.0.0.0: Theorem prover for intuitionistic propositional logic using G4ip

Safe HaskellSafe
LanguageHaskell2010

G4ipProver.Proposition

Description

Definition of propositions and some syntactic sugar

Documentation

data Prop Source #

Constructors

Atom String 
T 
F 
And Prop Prop 
Or Prop Prop 
Imp Prop Prop 
Instances
Eq Prop Source # 
Instance details

Defined in G4ipProver.Proposition

Methods

(==) :: Prop -> Prop -> Bool #

(/=) :: Prop -> Prop -> Bool #

Ord Prop Source # 
Instance details

Defined in G4ipProver.Proposition

Methods

compare :: Prop -> Prop -> Ordering #

(<) :: Prop -> Prop -> Bool #

(<=) :: Prop -> Prop -> Bool #

(>) :: Prop -> Prop -> Bool #

(>=) :: Prop -> Prop -> Bool #

max :: Prop -> Prop -> Prop #

min :: Prop -> Prop -> Prop #

Show Prop Source # 
Instance details

Defined in G4ipProver.Proposition

Methods

showsPrec :: Int -> Prop -> ShowS #

show :: Prop -> String #

showList :: [Prop] -> ShowS #

(/\) :: Prop -> Prop -> Prop infixr 3 Source #

(\/) :: Prop -> Prop -> Prop infixr 2 Source #

(==>) :: Prop -> Prop -> Prop infixr 1 Source #

(<==) :: Prop -> Prop -> Prop infixr 1 Source #

(<=>) :: Prop -> Prop -> Prop infixr 0 Source #

neg :: Prop -> Prop Source #