hol-1.4: Higher order logic

Safe Haskell	None
Language	Haskell2010

HOL.Thm

Description

Documentation

data Thm Source #

Instances

Instances details

Eq Thm Source #
Instance details Defined in HOL.Thm Methods (==) :: Thm -> Thm -> Bool # (/=) :: Thm -> Thm -> Bool #
Ord Thm Source #
Instance details Defined in HOL.Thm Methods compare :: Thm -> Thm -> Ordering # (<) :: Thm -> Thm -> Bool # (<=) :: Thm -> Thm -> Bool # (>) :: Thm -> Thm -> Bool # (>=) :: Thm -> Thm -> Bool # max :: Thm -> Thm -> Thm # min :: Thm -> Thm -> Thm #
Show Thm Source #
Instance details Defined in HOL.Thm Methods showsPrec :: Int -> Thm -> ShowS # show :: Thm -> String # showList :: [Thm] -> ShowS #
HasConsts Thm Source #
Instance details Defined in HOL.Thm Methods consts :: Thm -> Set Const Source #
HasOps Thm Source #
Instance details Defined in HOL.Thm Methods ops :: Thm -> Set TypeOp Source #
HasVars Thm Source #
Instance details Defined in HOL.Thm Methods vars :: Thm -> Set TypeVar Source #
HasFree Thm Source #
Instance details Defined in HOL.Thm Methods free :: Thm -> Set Var Source # freeIn :: Var -> Thm -> Bool Source # notFreeIn :: Var -> Thm -> Bool Source # closed :: Thm -> Bool Source #
CanSubst Thm Source #
Instance details Defined in HOL.Thm Methods basicSubst :: Thm -> Subst -> (Maybe Thm, Subst) Source # sharingSubst :: Thm -> Subst -> (Maybe Thm, Subst) Source # subst :: Subst -> Thm -> Maybe Thm Source # typeSubst :: TypeSubst -> Thm -> Maybe Thm Source # trySharingSubst :: Thm -> Subst -> (Thm, Subst) Source # trySubst :: Subst -> Thm -> Thm Source # tryTypeSubst :: TypeSubst -> Thm -> Thm Source #
Printable Thm Source #
Instance details Defined in HOL.Print Methods toDoc :: Thm -> Doc Source # toStringWith :: Style -> Thm -> String Source # toString :: Thm -> String Source #
Objective Thm Source #
Instance details Defined in HOL.OpenTheory.Article Methods toObject :: Thm -> Object Source # fromObject :: Object -> Maybe Thm Source #

assume :: Term -> Maybe Thm Source #

axiomOfChoice :: Thm Source #

axiomOfExtensionality :: Thm Source #

axiomOfInfinity :: Thm Source #

betaConv :: Term -> Maybe Thm Source #

concl :: Thm -> TermAlpha Source #

deductAntisym :: Thm -> Thm -> Thm Source #

defineConst :: Name -> Term -> Maybe (Const, Thm) Source #

defineTypeOp :: Name -> Name -> Name -> [TypeVar] -> Thm -> Maybe (TypeOp, Const, Const, Thm, Thm) Source #

dest :: Thm -> Sequent Source #

eqMp :: Thm -> Thm -> Maybe Thm Source #

hyp :: Thm -> Set TermAlpha Source #

mkAbs :: Var -> Thm -> Maybe Thm Source #

mkAbsUnsafe :: Var -> Thm -> Thm Source #

mkApp :: Thm -> Thm -> Maybe Thm Source #

mkAppUnsafe :: Thm -> Thm -> Thm Source #

nullHyp :: Thm -> Bool Source #

refl :: Term -> Thm Source #

standardAxioms :: Set Thm Source #

subst :: Subst -> Thm -> Thm Source #