Documentation

readTuple :: (Show a, Show b) => MSaxState a -> MSaxState b -> MSaxState (a, b)

readWord :: MSaxState String

readStr :: MSaxState String

readInt :: MSaxState Int

readInt' :: MSaxState Int

readMappedInt :: Map Int a -> MSaxState a

listToTypes :: Map Int HolType -> [Int] -> Maybe [HolType]

readSharedHolType :: Map Int String -> Map Int HolType -> MSaxState (Map Int HolType)

readParseType :: MSaxState HolParseType

readTermInfo :: MSaxState HolTermInfo

readSharedHolTerm :: Map Int HolType -> Map Int String -> Map Int Term -> MSaxState (Map Int Term)

importData :: HetcatsOpts -> FilePath -> IO ([(String, [(String, Term)])], [(String, String)])

getTypes :: Map String Int -> HolType -> Map String Int

mergeTypesOps :: (Map String Int, Map String HolType) -> (Map String Int, Map String HolType) -> (Map String Int, Map String HolType)

getOps :: Term -> (Map String Int, Map String HolType)

calcSig :: [(String, Term)] -> Sign

sigDepends :: Sign -> Sign -> Bool

prettifyTypeVarsTp :: HolType -> Map String String -> (HolType, Map String String)

prettifyTypeVarsTm :: Term -> Map String String -> (Term, Map String String)

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

treeLevels :: [(String, String)] -> Map Int [(String, String)]

makeNamedSentence :: String -> Term -> Named Sentence

_insNodeDG :: Sign -> [Named Sentence] -> String -> (DGraph, Map String (String, Node, DGNodeLab)) -> (DGraph, Map String (String, Node, DGNodeLab))

anaHolLightFile :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))