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

Safe HaskellNone
LanguageHaskell98

Data.Logic.Types.Harrison.Equal

Synopsis

Documentation

data FOLEQ Source

Constructors

EQUALS TermType TermType 
R String [TermType] 

Instances

Eq FOLEQ 
Ord FOLEQ 
Show FOLEQ 
HasFixity FOLEQ 
Pretty FOLEQ 
Constants FOLEQ 
Atom FOLEQ TermType String 
Apply FOLEQ PredName TermType

Using PredName for the predicate type is not quite appropriate here, but we need to implement this instance so we can use it as a superclass of AtomEq below.

AtomEq FOLEQ PredName TermType 
Show (Formula FOLEQ) 
HasFixity (Formula FOLEQ) 
Formula (Formula FOLEQ) FOLEQ => PropositionalFormula (Formula FOLEQ) FOLEQ 
Formula (Formula FOLEQ) FOLEQ => Literal (Formula FOLEQ) FOLEQ 

data PredName Source

Constructors

(:=:) 
Named String 

Instances

Eq PredName 
Data PredName 
Ord PredName 
Show PredName 
IsString PredName 
Pretty PredName 
Constants PredName 
Arity PredName 
Predicate PredName 
Typeable * PredName 
Apply FOLEQ PredName TermType

Using PredName for the predicate type is not quite appropriate here, but we need to implement this instance so we can use it as a superclass of AtomEq below.

AtomEq FOLEQ PredName TermType