logic-classes-1.4.7: Framework for propositional and first order logic, theorem proving

Safe HaskellNone

Data.Logic.Types.Harrison.Formulas.Propositional

Documentation

data Formula a Source

Constructors

F 
T 
Atom a 
Not (Formula a) 
And (Formula a) (Formula a) 
Or (Formula a) (Formula a) 
Imp (Formula a) (Formula a) 
Iff (Formula a) (Formula a) 

Instances

Eq a => Eq (Formula a) 
(Eq (Formula a), Ord a) => Ord (Formula a) 
Show (Formula String) 
Show (Formula Prop) 
Negatable (Formula atom) 
(Pretty atom, HasFixity atom, Ord atom) => HasFixity (Formula atom) 
(Pretty atom, HasFixity atom, Ord atom) => Pretty (Formula atom) 
Negatable (Formula a) => Combinable (Formula a) 
Constants (Formula a) 
(Pretty atom, HasFixity atom, Ord atom) => Formula (Formula atom) atom 
(Ord (Formula atom), Negatable (Formula atom), Constants (Formula atom), Pretty (Formula atom), HasFixity (Formula atom), Formula (Formula atom) atom, Combinable (Formula atom), Pretty atom, HasFixity atom, Ord atom) => PropositionalFormula (Formula atom) atom 
(Negatable (Formula atom), Constants (Formula atom), Formula (Formula atom) atom, Ord (Formula atom), HasFixity atom, Pretty atom, Ord atom) => Literal (Formula atom) atom