HOL.Theory

Documentation

data Theory

Constructors

Theory

Fields

• typeOpMap :: Map Name (Set TypeOp)
• constMap :: Map Name (Set Const)
• thmMap :: Map Sequent Thm

Instances

Eq Theory

Defined in HOL.Theory

Methods

(==) :: Theory -> Theory -> Bool

(/=) :: Theory -> Theory -> Bool

Ord Theory

Defined in HOL.Theory

Methods

compare :: Theory -> Theory -> Ordering

(<) :: Theory -> Theory -> Bool

(<=) :: Theory -> Theory -> Bool

(>) :: Theory -> Theory -> Bool

(>=) :: Theory -> Theory -> Bool

max :: Theory -> Theory -> Theory

min :: Theory -> Theory -> Theory

Show Theory

Defined in HOL.Theory

Methods

showsPrec :: Int -> Theory -> ShowS

show :: Theory -> String

showList :: [Theory] -> ShowS

HasConsts Theory

Defined in HOL.Theory

Methods

consts :: Theory -> Set Const

HasOps Theory

Defined in HOL.Theory

Methods

ops :: Theory -> Set TypeOp

Printable Theory

Defined in HOL.Theory

Methods

toDoc :: Theory -> Doc

toStringWith :: Style -> Theory -> String

toString :: Theory -> String

empty :: Theory

fromThmSet :: Set Thm -> Theory

union :: Theory -> Theory -> Theory

unionList :: [Theory] -> Theory

lookupTypeOp :: Theory -> Name -> Maybe TypeOp

lookupTypeOpUnsafe :: Theory -> Name -> TypeOp

lookupConst :: Theory -> Name -> Maybe Const

lookupConstUnsafe :: Theory -> Name -> Const

sequents :: Theory -> Set Sequent

thms :: Theory -> Set Thm

lookupThm :: Theory -> Sequent -> Maybe Thm

standard :: Theory