HOL.Const

Documentation

name :: Const -> Name

prov :: Const -> ConstProv

mkUndef :: Name -> Const

isUndef :: Const -> Bool

class HasConsts a where

Minimal complete definition

consts

Methods

consts :: a -> Set Const

Instances

HasConsts TermData

Methods

consts :: TermData -> Set Const

HasConsts Term

Methods

consts :: Term -> Set Const

HasConsts Const

Methods

consts :: Const -> Set Const

HasConsts TermAlpha

Methods

consts :: TermAlpha -> Set Const

HasConsts Sequent

Methods

consts :: Sequent -> Set Const

HasConsts Thm

Methods

consts :: Thm -> Set Const

HasConsts Theory

Methods

consts :: Theory -> Set Const

HasConsts a => HasConsts [a]

Methods

consts :: [a] -> Set Const

HasConsts a => HasConsts (Set a)

Methods

consts :: Set a -> Set Const

eqName :: Name

eq :: Const

selectName :: Name

select :: Const

primitives :: Set Const

condName :: Name

conjName :: Name

disjName :: Name

existsName :: Name

existsUniqueName :: Name

forallName :: Name

impName :: Name

negName :: Name

appendName :: Name

consName :: Name

pairName :: Name

composeName :: Name

funpowName :: Name

addName :: Name

bit0Name :: Name

bit1Name :: Name

divName :: Name

geName :: Name

gtName :: Name

leName :: Name

ltName :: Name

modName :: Name

multName :: Name

powerName :: Name

subName :: Name

zeroName :: Name

addRealName :: Name

divRealName :: Name

fromNaturalRealName :: Name

geRealName :: Name

gtRealName :: Name

leRealName :: Name

ltRealName :: Name

multRealName :: Name

powerRealName :: Name

subRealName :: Name

crossName :: Name

deleteName :: Name

differenceName :: Name

fromPredicateName :: Name

insertName :: Name

intersectName :: Name

memberName :: Name

properSubsetName :: Name

subsetName :: Name

unionName :: Name