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

HOL.Const

Description

 

Documentation

name :: Const -> Name Source #

prov :: Const -> ConstProv Source #

mkUndef :: Name -> Const Source #

isUndef :: Const -> Bool Source #

class HasConsts a where Source #

Methods

consts :: a -> Set Const Source #

Instances

Instances details
HasConsts TermData Source # 
Instance details

Defined in HOL.Const

Methods

consts :: TermData -> Set Const Source #

HasConsts Term Source # 
Instance details

Defined in HOL.Const

Methods

consts :: Term -> Set Const Source #

HasConsts Const Source # 
Instance details

Defined in HOL.Const

Methods

consts :: Const -> Set Const Source #

HasConsts TermAlpha Source # 
Instance details

Defined in HOL.TermAlpha

Methods

consts :: TermAlpha -> Set Const Source #

HasConsts Sequent Source # 
Instance details

Defined in HOL.Sequent

Methods

consts :: Sequent -> Set Const Source #

HasConsts Thm Source # 
Instance details

Defined in HOL.Thm

Methods

consts :: Thm -> Set Const Source #

HasConsts Theory Source # 
Instance details

Defined in HOL.Theory

Methods

consts :: Theory -> Set Const Source #

HasConsts a => HasConsts [a] Source # 
Instance details

Defined in HOL.Const

Methods

consts :: [a] -> Set Const Source #

HasConsts a => HasConsts (Set a) Source # 
Instance details

Defined in HOL.Const

Methods

consts :: Set a -> Set Const Source #

eqName :: Name Source #

eq :: Const Source #

selectName :: Name Source #

select :: Const Source #

primitives :: Set Const Source #

condName :: Name Source #

conjName :: Name Source #

disjName :: Name Source #

existsName :: Name Source #

existsUniqueName :: Name Source #

forallName :: Name Source #

impName :: Name Source #

negName :: Name Source #

appendName :: Name Source #

consName :: Name Source #

pairName :: Name Source #

composeName :: Name Source #

funpowName :: Name Source #

addName :: Name Source #

bit0Name :: Name Source #

bit1Name :: Name Source #

divName :: Name Source #

geName :: Name Source #

gtName :: Name Source #

leName :: Name Source #

ltName :: Name Source #

modName :: Name Source #

multName :: Name Source #

powerName :: Name Source #

subName :: Name Source #

sucName :: Name Source #

zeroName :: Name Source #

addRealName :: Name Source #

divRealName :: Name Source #

fromNaturalRealName :: Name Source #

geRealName :: Name Source #

gtRealName :: Name Source #

leRealName :: Name Source #

ltRealName :: Name Source #

multRealName :: Name Source #

powerRealName :: Name Source #

subRealName :: Name Source #

crossName :: Name Source #

deleteName :: Name Source #

differenceName :: Name Source #

fromPredicateName :: Name Source #

insertName :: Name Source #

intersectName :: Name Source #

memberName :: Name Source #

properSubsetName :: Name Source #

subsetName :: Name Source #

unionName :: Name Source #