Hets - the Heterogeneous Tool Set

Safe HaskellSafe

HolLight.Sublogic

Synopsis

Documentation

data HolLightSL Source #

sublogic

Constructors

Top 

Instances

Eq HolLightSL Source # 

Methods

(==) :: HolLightSL -> HolLightSL -> Bool

(/=) :: HolLightSL -> HolLightSL -> Bool

Ord HolLightSL Source # 
Show HolLightSL Source # 

Methods

showsPrec :: Int -> HolLightSL -> ShowS

show :: HolLightSL -> String

showList :: [HolLightSL] -> ShowS

Logic HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Source #

Instance of Logic for propositional logc

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 #

Comorphism HolLight2Isabelle HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #