Documentation

data HolLight2Isabelle

mapSentence :: Sign -> Sentence -> Result Sentence

mapHolSen :: Sentence -> Sentence

tp2DTyp :: HolType -> DTyp

constMap :: Map String VName

notIgnore :: [String]

ignore :: [String]

transConstS :: String -> HolType -> VName

typedName :: String -> HolType -> String

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

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

makeForAll :: Term -> [Term] -> Term -> Term

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

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

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

isAppT :: HolType -> Bool

isQuantifier :: Term -> Bool

varNames :: [Term] -> [String]

allVars :: Term -> [String]

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

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

bs :: BaseSig

mapSign :: Sign -> Sign

mapOps :: Map String HolType -> ConstTab

tp2Typ :: HolType -> Typ

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

mapTypes :: Map String Int -> TypeSig

mapNamedSen :: Named Sentence -> Named Sentence