Safe Haskell	Safe

HolLight.Sublogic

Synopsis

data HolLightSL = Top

Documentation

data HolLightSL Source #

sublogic

Constructors

Top

Instances

Instances details

Eq HolLightSL Source #
Instance details Defined in HolLight.Sublogic Methods (==) :: HolLightSL -> HolLightSL -> Bool (/=) :: HolLightSL -> HolLightSL -> Bool
Ord HolLightSL Source #
Instance details Defined in HolLight.Sublogic Methods compare :: HolLightSL -> HolLightSL -> Ordering (<) :: HolLightSL -> HolLightSL -> Bool (<=) :: HolLightSL -> HolLightSL -> Bool (>) :: HolLightSL -> HolLightSL -> Bool (>=) :: HolLightSL -> HolLightSL -> Bool max :: HolLightSL -> HolLightSL -> HolLightSL min :: HolLightSL -> HolLightSL -> HolLightSL
Show HolLightSL Source #
Instance details Defined in HolLight.Sublogic Methods showsPrec :: Int -> HolLightSL -> ShowS show :: HolLightSL -> String showList :: [HolLightSL] -> ShowS
Generic HolLightSL
Instance details Defined in HolLight.ATC_HolLight Associated Types type Rep HolLightSL :: Type -> Type Methods from :: HolLightSL -> Rep HolLightSL x to :: Rep HolLightSL x -> HolLightSL
FromJSON HolLightSL
Instance details Defined in HolLight.ATC_HolLight Methods parseJSON :: Value -> Parser HolLightSL parseJSONList :: Value -> Parser [HolLightSL]
ToJSON HolLightSL
Instance details Defined in HolLight.ATC_HolLight Methods toJSON :: HolLightSL -> Value toEncoding :: HolLightSL -> Encoding toJSONList :: [HolLightSL] -> Value toEncodingList :: [HolLightSL] -> Encoding
ShATermConvertible HolLightSL
Instance details Defined in HolLight.ATC_HolLight Methods toShATermAux :: ATermTable -> HolLightSL -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [HolLightSL] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, HolLightSL) fromShATermList' :: Int -> ATermTable -> (ATermTable, [HolLightSL])
SublogicName HolLightSL Source #
Instance details Defined in HolLight.Logic_HolLight Methods sublogicName :: HolLightSL -> String Source #
SemiLatticeWithTop HolLightSL Source #	Sublogics
Instance details Defined in HolLight.Logic_HolLight Methods lub :: HolLightSL -> HolLightSL -> HolLightSL Source # top :: HolLightSL Source #
ProjectSublogicM HolLightSL () Source #
Instance details Defined in HolLight.Logic_HolLight Methods projectSublogicM :: HolLightSL -> () -> Maybe () Source #
ProjectSublogic HolLightSL () Source #
Instance details Defined in HolLight.Logic_HolLight Methods projectSublogic :: HolLightSL -> () -> () Source #
ProjectSublogic HolLightSL Sign Source #
Instance details Defined in HolLight.Logic_HolLight Methods projectSublogic :: HolLightSL -> Sign -> Sign Source #
ProjectSublogic HolLightSL HolLightMorphism Source #
Instance details Defined in HolLight.Logic_HolLight Methods projectSublogic :: HolLightSL -> HolLightMorphism -> HolLightMorphism Source #
MinSublogic HolLightSL () Source #
Instance details Defined in HolLight.Logic_HolLight Methods minSublogic :: () -> HolLightSL Source #
MinSublogic HolLightSL Sign Source #
Instance details Defined in HolLight.Logic_HolLight Methods minSublogic :: Sign -> HolLightSL Source #
MinSublogic HolLightSL Sentence Source #
Instance details Defined in HolLight.Logic_HolLight Methods minSublogic :: Sentence -> HolLightSL Source #
MinSublogic HolLightSL HolLightMorphism Source #
Instance details Defined in HolLight.Logic_HolLight Methods minSublogic :: HolLightMorphism -> HolLightSL Source #
Logic HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Source #	Instance of Logic for propositional logc
Instance details Defined in HolLight.Logic_HolLight Methods parse_basic_sen :: HolLight -> Maybe (() -> AParser st Sentence) Source # stability :: HolLight -> Stability Source # data_logic :: HolLight -> Maybe AnyLogic Source # top_sublogic :: HolLight -> HolLightSL Source # all_sublogics :: HolLight -> [HolLightSL] Source # bottomSublogic :: HolLight -> Maybe HolLightSL Source # sublogicDimensions :: HolLight -> [[HolLightSL]] Source # parseSublogic :: HolLight -> String -> Maybe HolLightSL Source # proj_sublogic_epsilon :: HolLight -> HolLightSL -> Sign -> HolLightMorphism Source # provers :: HolLight -> [Prover Sign Sentence HolLightMorphism HolLightSL ()] Source # default_prover :: HolLight -> String Source # cons_checkers :: HolLight -> [ConsChecker Sign Sentence HolLightSL HolLightMorphism ()] Source # conservativityCheck :: HolLight -> [ConservativityChecker Sign Sentence HolLightMorphism] Source # empty_proof_tree :: HolLight -> () Source # syntaxTable :: HolLight -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: HolLight -> Maybe OMCD Source # export_symToOmdoc :: HolLight -> NameMap () -> () -> String -> Result TCElement Source # export_senToOmdoc :: HolLight -> NameMap () -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: HolLight -> SigMap () -> Sign -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: HolLight -> SigMapI () -> TCElement -> String -> Result () Source # omdocToSen :: HolLight -> SigMapI () -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: HolLight -> SigMapI () -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source # addOmdocToTheory :: HolLight -> SigMapI () -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source # sublogicOfTheo :: HolLight -> (Sign, [Sentence]) -> HolLightSL Source #
Comorphism HolLight2Isabelle HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.HolLight2Isabelle Methods sourceLogic :: HolLight2Isabelle -> HolLight Source # sourceSublogic :: HolLight2Isabelle -> HolLightSL Source # sourceSublogicLossy :: HolLight2Isabelle -> HolLightSL Source # minSourceTheory :: HolLight2Isabelle -> Maybe (LibName, String) Source # targetLogic :: HolLight2Isabelle -> Isabelle Source # mapSublogic :: HolLight2Isabelle -> HolLightSL -> Maybe () Source # map_theory :: HolLight2Isabelle -> (Sign0, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HolLight2Isabelle -> (Sign0, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HolLight2Isabelle -> HolLightMorphism -> Result IsabelleMorphism Source # map_sentence :: HolLight2Isabelle -> Sign0 -> Sentence0 -> Result Sentence Source # map_symbol :: HolLight2Isabelle -> Sign0 -> () -> Set () Source # extractModel :: HolLight2Isabelle -> Sign0 -> () -> Result (Sign0, [Named Sentence0]) Source # is_model_transportable :: HolLight2Isabelle -> Bool Source # has_model_expansion :: HolLight2Isabelle -> Bool Source # is_weakly_amalgamable :: HolLight2Isabelle -> Bool Source # constituents :: HolLight2Isabelle -> [String] Source # isInclusionComorphism :: HolLight2Isabelle -> Bool Source # rps :: HolLight2Isabelle -> Bool Source # eps :: HolLight2Isabelle -> Bool Source # isGTC :: HolLight2Isabelle -> Bool Source #
type Rep HolLightSL
Instance details Defined in HolLight.ATC_HolLight type Rep HolLightSL = D1 ('MetaData "HolLightSL" "HolLight.Sublogic" "main" 'False) (C1 ('MetaCons "Top" 'PrefixI 'False) (U1 :: Type -> Type))