module AbsHOL where
-- Haskell module generated by the BNF converter
newtype Idents = Idents String deriving (Eq,Ord,Show)
newtype PredId = PredId String deriving (Eq,Ord,Show)
newtype FunctId = FunctId String deriving (Eq,Ord,Show)
data PROGRAM =
PROGRAM [SENT]
deriving (Eq,Ord,Show)
data DEF =
DefSent Idents SENT
deriving (Eq,Ord,Show)
data SENT =
ASentPred PredId [TERMS]
| TrueSent
| FalseSent
| IdentSent Idents
| ASentEq TERM TERM
| NegSent SENT
| IfSent SENT SENT SENT
| AndSent SENT SENT
| OrSent SENT SENT
| ImpSent SENT SENT
| LetSent [DEF] SENT
| ForallSent [TERM] SENT
| ExistsSent [TERM] SENT
deriving (Eq,Ord,Show)
data TERM =
FunctTerm FunctId [TERMS]
| ConstVarTerm Idents
deriving (Eq,Ord,Show)
data TERMS =
Terms [TERM]
deriving (Eq,Ord,Show)