Safe Haskell | Safe |
---|
- newtype Name = N String
- data Ident = I Name [Integer]
- data Quant
- data Conn
- data Formula
- type Sort = Ident
- data Binder = Bind {}
- data Term
- data Literal
- data Annot = Attr {}
- data FunDecl = FunDecl {}
- data PredDecl = PredDecl {}
- data Status
- data Command
- = CmdLogic Ident
- | CmdAssumption Formula
- | CmdFormula Formula
- | CmdStatus Status
- | CmdExtraSorts [Sort]
- | CmdExtraFuns [FunDecl]
- | CmdExtraPreds [PredDecl]
- | CmdNotes String
- | CmdAnnot Annot
- data Script = Script {
- scrName :: Ident
- scrCommands :: [Command]
- (===) :: Term -> Term -> Formula
- (=/=) :: Term -> Term -> Formula
- (.<.) :: Term -> Term -> Formula
- (.>.) :: Term -> Term -> Formula
- tInt :: Sort
- funDef :: Ident -> [Sort] -> Sort -> Command
- constDef :: Ident -> Sort -> Command
- logic :: Ident -> Command
- assume :: Formula -> Command
- goal :: Formula -> Command
- class PP t where