hol-1.4: Higher order logic
Safe HaskellSafe-Inferred
LanguageHaskell2010

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 #