HOL.TermData
Description
mkConst :: Const -> Type -> TermData Source #
destConst :: TermData -> Maybe (Const, Type) Source #
isConst :: TermData -> Bool Source #
destGivenConst :: Const -> TermData -> Maybe Type Source #
isGivenConst :: Const -> TermData -> Bool Source #
mkVar :: Var -> TermData Source #
destVar :: TermData -> Maybe Var Source #
isVar :: TermData -> Bool Source #
eqVar :: Var -> TermData -> Bool Source #
mkApp :: Term -> Term -> Maybe TermData Source #
destApp :: TermData -> Maybe (Term, Term) Source #
isApp :: TermData -> Bool Source #
mkAbs :: Var -> Term -> TermData Source #
destAbs :: TermData -> Maybe (Var, Term) Source #
isAbs :: TermData -> Bool Source #
size :: TermData -> Size Source #
typeOf :: TermData -> Type Source #
freeInMultiple :: Var -> TermData -> Bool Source #