HOL.Type
Description
dest :: Type -> TypeData Source #
mk :: TypeData -> Type Source #
mkVar :: TypeVar -> Type Source #
destVar :: Type -> Maybe TypeVar Source #
isVar :: Type -> Bool Source #
eqVar :: TypeVar -> Type -> Bool Source #
mkOp :: TypeOp -> [Type] -> Type Source #
destOp :: Type -> Maybe (TypeOp, [Type]) Source #
isOp :: Type -> Bool Source #
destGivenOp :: TypeOp -> Type -> Maybe [Type] Source #
isGivenOp :: TypeOp -> Type -> Bool Source #
size :: Type -> Size Source #
isNullaryOp :: TypeOp -> Type -> Bool Source #
destUnaryOp :: TypeOp -> Type -> Maybe Type Source #
isUnaryOp :: TypeOp -> Type -> Bool Source #
destBinaryOp :: TypeOp -> Type -> Maybe (Type, Type) Source #
isBinaryOp :: TypeOp -> Type -> Bool Source #
alpha :: Type Source #
beta :: Type Source #
bool :: Type Source #
isBool :: Type -> Bool Source #
mkPred :: Type -> Type Source #
destPred :: Type -> Maybe Type Source #
isPred :: Type -> Bool Source #
mkRel :: Type -> Type -> Type Source #
destRel :: Type -> Maybe (Type, Type) Source #
isRel :: Type -> Bool Source #
mkFun :: Type -> Type -> Type Source #
destFun :: Type -> Maybe (Type, Type) Source #
isFun :: Type -> Bool Source #
domain :: Type -> Maybe Type Source #
range :: Type -> Maybe Type Source #
listMkFun :: [Type] -> Type -> Type Source #
stripFun :: Type -> ([Type], Type) Source #
ind :: Type Source #
isInd :: Type -> Bool Source #
mkEq :: Type -> Type Source #
destEq :: Type -> Maybe Type Source #
isEq :: Type -> Bool Source #
mkSelect :: Type -> Type Source #
destSelect :: Type -> Maybe Type Source #
isSelect :: Type -> Bool Source #