Hets - the Heterogeneous Tool Set
Safe HaskellSafe

HolLight.Sublogic

Synopsis

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

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

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

ProjectSublogic HolLightSL HolLightMorphism Source # 
Instance details

Defined in HolLight.Logic_HolLight

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

MinSublogic HolLightSL Sentence Source # 
Instance details

Defined in HolLight.Logic_HolLight

MinSublogic HolLightSL HolLightMorphism Source # 
Instance details

Defined in HolLight.Logic_HolLight

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

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))