Safe Haskell	None
Language	Haskell2010

HOL.OpenTheory.Article

Description

Documentation

newtype Number Source #

Constructors

Number Integer

Instances

Instances details

Eq Number Source #
Instance details Defined in HOL.OpenTheory.Article Methods (==) :: Number -> Number -> Bool # (/=) :: Number -> Number -> Bool #
Ord Number Source #
Instance details Defined in HOL.OpenTheory.Article Methods compare :: Number -> Number -> Ordering # (<) :: Number -> Number -> Bool # (<=) :: Number -> Number -> Bool # (>) :: Number -> Number -> Bool # (>=) :: Number -> Number -> Bool # max :: Number -> Number -> Number # min :: Number -> Number -> Number #
Show Number Source #
Instance details Defined in HOL.OpenTheory.Article Methods showsPrec :: Int -> Number -> ShowS # show :: Number -> String # showList :: [Number] -> ShowS #
Parsable Number Source #
Instance details Defined in HOL.OpenTheory.Article Methods parser :: Parsec Text st Number Source # fromText :: Text -> Maybe Number Source # fromString :: String -> Maybe Number Source # fromStringUnsafe :: String -> Number Source # fromTextFile :: FilePath -> IO Number Source #
Printable Number Source #
Instance details Defined in HOL.OpenTheory.Article Methods toDoc :: Number -> Doc Source # toStringWith :: Style -> Number -> String Source # toString :: Number -> String Source #
Objective Number Source #
Instance details Defined in HOL.OpenTheory.Article Methods toObject :: Number -> Object Source # fromObject :: Object -> Maybe Number Source #

data Object Source #

Constructors

NumberObject Number
NameObject Name
ListObject [Object]
TypeOpObject TypeOp
TypeObject Type
ConstObject Const
VarObject Var
TermObject Term
ThmObject Thm

Instances

Instances details

Eq Object Source #
Instance details Defined in HOL.OpenTheory.Article Methods (==) :: Object -> Object -> Bool # (/=) :: Object -> Object -> Bool #
Ord Object Source #
Instance details Defined in HOL.OpenTheory.Article Methods compare :: Object -> Object -> Ordering # (<) :: Object -> Object -> Bool # (<=) :: Object -> Object -> Bool # (>) :: Object -> Object -> Bool # (>=) :: Object -> Object -> Bool # max :: Object -> Object -> Object # min :: Object -> Object -> Object #
Show Object Source #
Instance details Defined in HOL.OpenTheory.Article Methods showsPrec :: Int -> Object -> ShowS # show :: Object -> String # showList :: [Object] -> ShowS #
Printable Object Source #
Instance details Defined in HOL.OpenTheory.Article Methods toDoc :: Object -> Doc Source # toStringWith :: Style -> Object -> String Source # toString :: Object -> String Source #
Objective Object Source #
Instance details Defined in HOL.OpenTheory.Article Methods toObject :: Object -> Object Source # fromObject :: Object -> Maybe Object Source #

class Objective a where Source #

Methods

toObject :: a -> Object Source #

fromObject :: Object -> Maybe a Source #

Instances

Instances details

Objective Name Source #
Instance details Defined in HOL.OpenTheory.Article Methods toObject :: Name -> Object Source # fromObject :: Object -> Maybe Name Source #
Objective Term Source #
Instance details Defined in HOL.OpenTheory.Article Methods toObject :: Term -> Object Source # fromObject :: Object -> Maybe Term Source #
Objective Const Source #
Instance details Defined in HOL.OpenTheory.Article Methods toObject :: Const -> Object Source # fromObject :: Object -> Maybe Const Source #
Objective Var Source #
Instance details Defined in HOL.OpenTheory.Article Methods toObject :: Var -> Object Source # fromObject :: Object -> Maybe Var Source #
Objective Type Source #
Instance details Defined in HOL.OpenTheory.Article Methods toObject :: Type -> Object Source # fromObject :: Object -> Maybe Type Source #
Objective TypeOp Source #
Instance details Defined in HOL.OpenTheory.Article Methods toObject :: TypeOp -> Object Source # fromObject :: Object -> Maybe TypeOp Source #
Objective Thm Source #
Instance details Defined in HOL.OpenTheory.Article Methods toObject :: Thm -> Object Source # fromObject :: Object -> Maybe Thm Source #
Objective Object Source #
Instance details Defined in HOL.OpenTheory.Article Methods toObject :: Object -> Object Source # fromObject :: Object -> Maybe Object Source #
Objective Number Source #
Instance details Defined in HOL.OpenTheory.Article Methods toObject :: Number -> Object Source # fromObject :: Object -> Maybe Number Source #
Objective a => Objective [a] Source #
Instance details Defined in HOL.OpenTheory.Article Methods toObject :: [a] -> Object Source # fromObject :: Object -> Maybe [a] Source #
(Objective a, Objective b) => Objective (a, b) Source #
Instance details Defined in HOL.OpenTheory.Article Methods toObject :: (a, b) -> Object Source # fromObject :: Object -> Maybe (a, b) Source #

sequentObject :: Object -> Object -> Maybe Sequent Source #

pushObject :: Objective a => a -> [Object] -> [Object] Source #

push2Object :: (Objective a, Objective b) => a -> b -> [Object] -> [Object] Source #

push3Object :: (Objective a, Objective b, Objective c) => a -> b -> c -> [Object] -> [Object] Source #

push4Object :: (Objective a, Objective b, Objective c, Objective d) => a -> b -> c -> d -> [Object] -> [Object] Source #

push5Object :: (Objective a, Objective b, Objective c, Objective d, Objective e) => a -> b -> c -> d -> e -> [Object] -> [Object] Source #

popObject :: Objective a => [Object] -> Maybe (a, [Object]) Source #

pop2Object :: (Objective a, Objective b) => [Object] -> Maybe (a, b, [Object]) Source #

pop3Object :: (Objective a, Objective b, Objective c) => [Object] -> Maybe (a, b, c, [Object]) Source #

pop4Object :: (Objective a, Objective b, Objective c, Objective d) => [Object] -> Maybe (a, b, c, d, [Object]) Source #

pop5Object :: (Objective a, Objective b, Objective c, Objective d, Objective e) => [Object] -> Maybe (a, b, c, d, e, [Object]) Source #

data Command Source #

Instances

Instances details

Eq Command Source #
Instance details Defined in HOL.OpenTheory.Article Methods (==) :: Command -> Command -> Bool # (/=) :: Command -> Command -> Bool #
Ord Command Source #
Instance details Defined in HOL.OpenTheory.Article Methods compare :: Command -> Command -> Ordering # (<) :: Command -> Command -> Bool # (<=) :: Command -> Command -> Bool # (>) :: Command -> Command -> Bool # (>=) :: Command -> Command -> Bool # max :: Command -> Command -> Command # min :: Command -> Command -> Command #
Show Command Source #
Instance details Defined in HOL.OpenTheory.Article Methods showsPrec :: Int -> Command -> ShowS # show :: Command -> String # showList :: [Command] -> ShowS #
Parsable Command Source #
Instance details Defined in HOL.OpenTheory.Article Methods parser :: Parsec Text st Command Source # fromText :: Text -> Maybe Command Source # fromString :: String -> Maybe Command Source # fromStringUnsafe :: String -> Command Source # fromTextFile :: FilePath -> IO Command Source #
Printable Command Source #
Instance details Defined in HOL.OpenTheory.Article Methods toDoc :: Command -> Doc Source # toStringWith :: Style -> Command -> String Source # toString :: Command -> String Source #

regularCommands :: [(Command, String)] Source #

type Version = Number Source #

supportedCommand :: Version -> Command -> Bool Source #

versionCommand :: Version -> Command -> Maybe Command Source #

data State Source #

Constructors

State
Fields stack :: [Object] dict :: Map Number Object theorems :: Set Thm

Instances

Instances details

Eq State Source #
Instance details Defined in HOL.OpenTheory.Article Methods (==) :: State -> State -> Bool # (/=) :: State -> State -> Bool #
Ord State Source #
Instance details Defined in HOL.OpenTheory.Article Methods compare :: State -> State -> Ordering # (<) :: State -> State -> Bool # (<=) :: State -> State -> Bool # (>) :: State -> State -> Bool # (>=) :: State -> State -> Bool # max :: State -> State -> State # min :: State -> State -> State #
Show State Source #
Instance details Defined in HOL.OpenTheory.Article Methods showsPrec :: Int -> State -> ShowS # show :: State -> String # showList :: [State] -> ShowS #
Printable State Source #
Instance details Defined in HOL.OpenTheory.Article Methods toDoc :: State -> Doc Source # toStringWith :: Style -> State -> String Source # toString :: State -> String Source #

pushState :: Objective a => a -> State -> State Source #

push2State :: (Objective a, Objective b) => a -> b -> State -> State Source #

push5State :: (Objective a, Objective b, Objective c, Objective d, Objective e) => a -> b -> c -> d -> e -> State -> State Source #

popState :: Objective a => State -> Maybe (a, State) Source #

pop2State :: (Objective a, Objective b) => State -> Maybe (a, b, State) Source #

pop3State :: (Objective a, Objective b, Objective c) => State -> Maybe (a, b, c, State) Source #

pop5State :: (Objective a, Objective b, Objective c, Objective d, Objective e) => State -> Maybe (a, b, c, d, e, State) Source #

peekState :: Objective a => State -> Maybe a Source #

defState :: Number -> Object -> State -> State Source #

refState :: Number -> State -> Maybe Object Source #

removeState :: Number -> State -> Maybe (Object, State) Source #

thmState :: Thm -> State -> State Source #

initialState :: State Source #

executeCommand :: Theory -> Interpret -> State -> Command -> Maybe State Source #

type LineNumber = Integer Source #

readArticle :: Theory -> Interpret -> FilePath -> IO (Set Thm) Source #

NumberCommand Number
NameCommand Name
AbsTermCommand
AbsThmCommand
AppTermCommand
AppThmCommand
AssumeCommand
AxiomCommand
BetaConvCommand
ConsCommand
ConstCommand
ConstTermCommand
DeductAntisymCommand
DefCommand
DefineConstCommand
DefineConstListCommand
DefineTypeOpCommand
EqMpCommand
HdTlCommand
NilCommand
OpTypeCommand
PopCommand
PragmaCommand
ProveHypCommand
RefCommand
ReflCommand
RemoveCommand
SubstCommand
SymCommand
ThmCommand
TransCommand
TypeOpCommand
VarCommand
VarTermCommand
VarTypeCommand
VersionCommand
DefineTypeOpLegacyCommand