HOL.TermAlpha

Documentation

newtype TermAlpha

Constructors

TermAlpha Term

Instances

Eq TermAlpha

Methods

(==) :: TermAlpha -> TermAlpha -> Bool

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

Ord 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

Methods

showsPrec :: Int -> TermAlpha -> ShowS

show :: TermAlpha -> String

showList :: [TermAlpha] -> ShowS

HasOps TermAlpha

Methods

ops :: TermAlpha -> Set TypeOp

HasVars TermAlpha

Methods

vars :: TermAlpha -> Set TypeVar

HasFree TermAlpha

Methods

free :: TermAlpha -> Set Var

freeIn :: Var -> TermAlpha -> Bool

notFreeIn :: Var -> TermAlpha -> Bool

closed :: TermAlpha -> Bool

HasConsts TermAlpha

Methods

consts :: TermAlpha -> Set Const

CanSubst TermAlpha

Methods

basicSubst :: TermAlpha -> Subst -> (Maybe TermAlpha, Subst)

sharingSubst :: TermAlpha -> Subst -> (Maybe TermAlpha, Subst)

subst :: Subst -> TermAlpha -> Maybe TermAlpha

typeSubst :: TypeSubst -> TermAlpha -> Maybe TermAlpha

trySharingSubst :: TermAlpha -> Subst -> (TermAlpha, Subst)

trySubst :: Subst -> TermAlpha -> TermAlpha

tryTypeSubst :: TypeSubst -> TermAlpha -> TermAlpha

Printable TermAlpha

Methods

toDoc :: TermAlpha -> Doc

toStringWith :: Style -> TermAlpha -> String

toString :: TermAlpha -> String

mk :: Term -> TermAlpha

dest :: TermAlpha -> Term

typeOf :: TermAlpha -> Type

isBool :: TermAlpha -> Bool

axiomOfExtensionality :: TermAlpha

axiomOfChoice :: TermAlpha

axiomOfInfinity :: TermAlpha

standardAxioms :: Set TermAlpha

standardAxiomName :: TermAlpha -> String