Hets - the Heterogeneous Tool Set

Copyright(c) Jonathan von Schroeder DFKI GmbH 2010
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerjonathan.von_schroeder@dfki.de
Stabilityexperimental
Portabilityportable
Safe HaskellSafe

HolLight.Helper

Description

 

Documentation

names :: [String] Source #

freeName :: [String] -> String Source #

fromRight :: Either t t1 -> t1 Source #

isPrefix :: Term -> Bool 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 #

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 #

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

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

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

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

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

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

destForall :: Term -> Maybe (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 #

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 #