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

Show HolLight2Isabelle Source # 

Methods

showsPrec :: Int -> HolLight2Isabelle -> ShowS

show :: HolLight2Isabelle -> String

showList :: [HolLight2Isabelle] -> ShowS

Language HolLight2Isabelle Source # 
Comorphism HolLight2Isabelle HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () () 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 #

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

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

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

isAppT :: HolType -> Bool Source #

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

allVars :: Term -> [String] Source #

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

mapOps :: Map String HolType -> ConstTab Source #

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

mapTypes :: Map String Int -> TypeSig Source #