hol-1.4: Higher order logic
Safe HaskellNone
LanguageHaskell2010

HOL.Term

Description

 

Documentation

dest :: Term -> TermData Source #

mk :: TermData -> Term Source #

mkConst :: Const -> Type -> Term Source #

destConst :: Term -> Maybe (Const, Type) Source #

isConst :: Term -> Bool Source #

destGivenConst :: Const -> Term -> Maybe Type Source #

isGivenConst :: Const -> Term -> Bool Source #

mkVar :: Var -> Term Source #

destVar :: Term -> Maybe Var Source #

isVar :: Term -> Bool Source #

eqVar :: Var -> Term -> Bool Source #

mkApp :: Term -> Term -> Maybe Term Source #

mkAppUnsafe :: Term -> Term -> Term Source #

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

isApp :: Term -> Bool Source #

rator :: Term -> Maybe Term Source #

rand :: Term -> Maybe Term Source #

land :: Term -> Maybe Term Source #

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

listMkAppUnsafe :: Term -> [Term] -> Term Source #

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

mkAbs :: Var -> Term -> Term Source #

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

isAbs :: Term -> Bool Source #

listMkAbs :: [Var] -> Term -> Term Source #

stripAbs :: Term -> ([Var], Term) Source #

size :: Term -> Size Source #

typeOf :: Term -> Type Source #

isBool :: Term -> Bool Source #

sameType :: Term -> Term -> Bool Source #

sameTypeVar :: Var -> Term -> Bool Source #

freeInMultiple :: Var -> Term -> Bool Source #

freeInOnce :: Var -> Term -> Bool Source #

alphaCompare :: Term -> Term -> Ordering Source #

alphaEqual :: Term -> Term -> Bool Source #

renameFresh :: Term -> Term Source #

mkEqConst :: Type -> Term Source #

destEqConst :: Term -> Maybe Type Source #

isEqConst :: Term -> Bool Source #

mkEq :: Term -> Term -> Maybe Term Source #

mkEqUnsafe :: Term -> Term -> Term Source #

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

isEq :: Term -> Bool Source #

lhs :: Term -> Maybe Term Source #

rhs :: Term -> Maybe Term Source #

rhsUnsafe :: Term -> Term Source #

mkRefl :: Term -> Term Source #

destRefl :: Term -> Maybe Term Source #

isRefl :: Term -> Bool Source #

mkSelectConst :: Type -> Term Source #

destSelectConst :: Term -> Maybe Type Source #

isSelectConst :: Term -> Bool Source #

mkSelect :: Var -> Term -> Term Source #

destSelect :: Term -> Maybe (Var, Term) Source #

isSelect :: Term -> Bool Source #