Data.Logic.Types.Harrison.FOL

Documentation

data TermType

Constructors

Var String

Fn Function [TermType]

Instances

Eq TermType

Ord TermType

Show TermType

Pretty TermType

Atom FOLEQ TermType String

Term TermType String Function

Apply FOL String TermType

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

data FOL

Constructors

R String [TermType]

Instances

Eq FOL

Ord FOL

Show FOL

HasFixity FOL

Pretty FOL

Constants FOL

Apply FOL String TermType

data Function

The Harrison book uses String for atomic function, but we need something a little more type safe because of our Skolem class.

Constructors

FName String

Skolem String

Instances

Eq Function

Data Function

Ord Function

Show Function

Pretty Function

Skolem Function String

Function Function String

Term TermType String Function