hol-1.4: Higher order logic

Safe Haskell	None
Language	Haskell2010

HOL.TermAlpha

Description

Documentation

newtype TermAlpha Source #

Constructors

Instances

Instances details

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

mk :: Term -> TermAlpha Source #

dest :: TermAlpha -> Term Source #

typeOf :: TermAlpha -> Type Source #

isBool :: TermAlpha -> Bool Source #

axiomOfExtensionality :: TermAlpha Source #

axiomOfChoice :: TermAlpha Source #

axiomOfInfinity :: TermAlpha Source #

standardAxioms :: Set TermAlpha Source #

standardAxiomName :: TermAlpha -> String Source #