Hets - the Heterogeneous Tool Set
Copyright(c) Jonathan von Schroeder and M. Codescu DFKI 2010
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerjonathan.von_schroeder@dfki.de
Stabilityprovisional
Portabilitynon-portable (imports Logic.Logic)
Safe HaskellNone

Comorphisms.HolLight2Isabelle

Description

 

Documentation

data HolLight2Isabelle Source #

Constructors

HolLight2Isabelle 

Instances

Instances details
Show HolLight2Isabelle Source # 
Instance details

Defined in Comorphisms.HolLight2Isabelle

Methods

showsPrec :: Int -> HolLight2Isabelle -> ShowS

show :: HolLight2Isabelle -> String

showList :: [HolLight2Isabelle] -> ShowS

Language HolLight2Isabelle Source # 
Instance details

Defined in Comorphisms.HolLight2Isabelle

Methods

language_name :: HolLight2Isabelle -> String Source #

description :: HolLight2Isabelle -> String 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 #

mapSentence :: Sign -> Sentence -> Result Sentence Source #

mapHolSen :: Sentence -> Sentence Source #

tp2DTyp :: HolType -> DTyp Source #

constMap :: Map String VName Source #

notIgnore :: [String] Source #

ignore :: [String] Source #

transConstS :: String -> HolType -> VName Source #

typedName :: String -> HolType -> String Source #

unpack_gabs :: Term -> [String] -> (Term, [Term], Term, Term) Source #

unpack_gabs' :: Term -> [String] -> [Term] -> Maybe (Term, [Term], Term) Source #

makeForAll :: Term -> [Term] -> Term -> Term Source #

handleGabs :: Bool -> Term -> [String] -> Term Source #

mkAbs :: Term -> [String] -> Term Source #

mkQuantifier :: Term -> [String] -> Term Source #

isAppT :: HolType -> Bool Source #

isQuantifier :: Term -> Bool Source #

varNames :: [Term] -> [String] Source #

allVars :: Term -> [String] Source #

translateTerm :: Term -> [String] -> Term Source #

mapTheory :: (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #

bs :: BaseSig Source #

mapSign :: Sign -> Sign Source #

mapOps :: Map String HolType -> ConstTab Source #

tp2Typ :: HolType -> Typ Source #

arity2tp :: Int -> [(IsaClass, [(Typ, Sort)])] Source #

mapTypes :: Map String Int -> TypeSig Source #

mapNamedSen :: Named Sentence -> Named Sentence Source #