HOL.Sequent

Documentation

data Sequent

Constructors

Sequent

Fields

• concl :: TermAlpha
• hyp :: Set TermAlpha

Instances

Eq Sequent

Methods

(==) :: Sequent -> Sequent -> Bool

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

Ord Sequent

Methods

compare :: Sequent -> Sequent -> Ordering

(<) :: Sequent -> Sequent -> Bool

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

(>) :: Sequent -> Sequent -> Bool

(>=) :: Sequent -> Sequent -> Bool

max :: Sequent -> Sequent -> Sequent

min :: Sequent -> Sequent -> Sequent

Show Sequent

Methods

showsPrec :: Int -> Sequent -> ShowS

show :: Sequent -> String

showList :: [Sequent] -> ShowS

HasOps Sequent

Methods

ops :: Sequent -> Set TypeOp

HasVars Sequent

Methods

vars :: Sequent -> Set TypeVar

HasFree Sequent

Methods

free :: Sequent -> Set Var

freeIn :: Var -> Sequent -> Bool

notFreeIn :: Var -> Sequent -> Bool

closed :: Sequent -> Bool

HasConsts Sequent

Methods

consts :: Sequent -> Set Const

CanSubst Sequent

Methods

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

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

subst :: Subst -> Sequent -> Maybe Sequent

typeSubst :: TypeSubst -> Sequent -> Maybe Sequent

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

trySubst :: Subst -> Sequent -> Sequent

tryTypeSubst :: TypeSubst -> Sequent -> Sequent

Printable Sequent

Methods

toDoc :: Sequent -> Doc

toStringWith :: Style -> Sequent -> String

toString :: Sequent -> String

mk :: Set TermAlpha -> TermAlpha -> Maybe Sequent

mkUnsafe :: Set TermAlpha -> TermAlpha -> Sequent

dest :: Sequent -> (Set TermAlpha, TermAlpha)

nullHyp :: Sequent -> Bool

mkNullHyp :: TermAlpha -> Maybe Sequent

mkNullHypUnsafe :: TermAlpha -> Sequent

axiomOfExtensionality :: Sequent

axiomOfChoice :: Sequent

axiomOfInfinity :: Sequent

standardAxioms :: Set Sequent