Documentation

names :: [String] Source #

freeName :: [String] -> String Source #

fromRight :: Either t t1 -> t1 Source #

isPrefix :: Term -> Bool Source #

ppPrintType :: HolType -> Doc Source #

soc :: String -> Bool -> [Doc] -> Doc Source #

sot :: Int -> HolType -> Doc Source #

revAssocd :: Eq t1 => t1 -> [(t, t1)] -> t -> t Source #

destVar :: Term -> Maybe (String, HolType) Source #

isVar :: Term -> Bool Source #

frees :: Term -> [Term] Source #

vfreeIn :: Term -> Term -> Bool Source #

variant :: [Term] -> Term -> Maybe Term Source #

vsubst :: [(Term, Term)] -> Term -> Maybe Term Source #

destComb :: Term -> Maybe (Term, Term) Source #

isComb :: Term -> Bool Source #

destConst :: Term -> Maybe (String, HolType) Source #

isConst :: Term -> Bool Source #

destAbs :: Term -> Maybe (Term, Term) Source #

isAbs :: Term -> Bool Source #

rator :: Term -> Maybe Term Source #

rand :: Term -> Maybe Term Source #

splitlist :: (t -> Maybe (a, t)) -> t -> ([a], t) Source #

revSplitlist :: (t -> Maybe (t, t1)) -> t -> (t, [t1]) Source #

typeOf :: Term -> Maybe HolType Source #

destType :: HolType -> Maybe (String, [HolType]) Source #

destVartype :: HolType -> Maybe String Source #

typeSubst :: [(HolType, HolType)] -> HolType -> HolType Source #

mkEq :: (Term, Term) -> Maybe Term Source #

inst :: [(HolType, HolType)] -> Term -> Either Term Term Source #

mkComb :: (Term, Term) -> Maybe Term Source #

eqType :: HolType Source #

mkConst :: (String, [(HolType, HolType)]) -> Maybe Term Source #

destBinder :: String -> Term -> Maybe (Term, Term) Source #

destExists :: Term -> Maybe (Term, Term) Source #

stripExists :: Term -> ([Term], Term) Source #

destForall :: Term -> Maybe (Term, Term) Source #

stripForall :: Term -> ([Term], Term) Source #

stripComb :: Term -> (Term, [Term]) Source #

body :: Term -> Maybe Term Source #

destNumeral :: Term -> Maybe Integer Source #

destBinary' :: String -> Term -> Maybe (Term, Term) Source #

destCons :: Term -> Maybe (Term, Term) Source #

destList :: Term -> Maybe [Term] Source #

destGabs :: Term -> Maybe (Term, Term) Source #

isGabs :: Term -> Bool Source #

stripGabs :: Term -> ([Term], Term) Source #

destFunTy :: HolType -> Maybe (HolType, HolType) Source #

destLet :: Term -> Maybe ([(Term, Term)], Term) Source #

nameOf :: Term -> String Source #

reverseInterface :: (String, Term) -> (String, Maybe HolParseType) Source #

destBinary :: Term -> Term -> Maybe (Term, Term) Source #

powerof10 :: Integer -> Bool Source #

boolOfTerm :: Term -> Maybe Bool Source #

codeOfTerm :: Num b => Term -> Maybe b Source #

randRator :: Term -> Maybe Term Source #

destClause :: Term -> Maybe [Term] Source #

destClauses :: Term -> Maybe [[Term]] Source #

aright :: Term -> Bool Source #

getPrec :: Term -> Int Source #

parsesAsBinder :: Term -> Bool Source #

canGetInfixStatus :: Term -> Bool Source #