hol-1.4: Higher order logic

Safe Haskell	Safe-Inferred
Language	Haskell2010

HOL.TypeOp

Description

Documentation

name :: TypeOp -> Name Source #

prov :: TypeOp -> TypeOpProv Source #

mkUndef :: Name -> TypeOp Source #

isUndef :: TypeOp -> Bool Source #

class HasOps a where Source #

Methods

ops :: a -> Set TypeOp Source #

Instances

Instances details

HasOps TermData Source #
Instance details Defined in HOL.TypeOp Methods ops :: TermData -> Set TypeOp Source #
HasOps Term Source #
Instance details Defined in HOL.TypeOp Methods ops :: Term -> Set TypeOp Source #
HasOps Var Source #
Instance details Defined in HOL.TypeOp Methods ops :: Var -> Set TypeOp Source #
HasOps TypeData Source #
Instance details Defined in HOL.TypeOp Methods ops :: TypeData -> Set TypeOp Source #
HasOps Type Source #
Instance details Defined in HOL.TypeOp Methods ops :: Type -> Set TypeOp Source #
HasOps TypeOp Source #
Instance details Defined in HOL.TypeOp Methods ops :: TypeOp -> Set TypeOp Source #
HasOps TermAlpha Source #
Instance details Defined in HOL.TermAlpha Methods ops :: TermAlpha -> Set TypeOp Source #
HasOps Sequent Source #
Instance details Defined in HOL.Sequent Methods ops :: Sequent -> Set TypeOp Source #
HasOps Thm Source #
Instance details Defined in HOL.Thm Methods ops :: Thm -> Set TypeOp Source #
HasOps Theory Source #
Instance details Defined in HOL.Theory Methods ops :: Theory -> Set TypeOp Source #
HasOps a => HasOps [a] Source #
Instance details Defined in HOL.TypeOp Methods ops :: [a] -> Set TypeOp Source #
HasOps a => HasOps (Set a) Source #
Instance details Defined in HOL.TypeOp Methods ops :: Set a -> Set TypeOp Source #

boolName :: Name Source #

bool :: TypeOp Source #

funName :: Name Source #

fun :: TypeOp Source #

indName :: Name Source #

ind :: TypeOp Source #

primitives :: Set TypeOp Source #

productName :: Name Source #

sumName :: Name Source #

naturalName :: Name Source #