hol-1.4: Higher order logic

Safe Haskell	None
Language	Haskell2010

HOL.Sequent

Description

Documentation

data Sequent Source #

Constructors

Sequent
Fields concl :: TermAlpha hyp :: Set TermAlpha

Instances

Instances details

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

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

mkUnsafe :: Set TermAlpha -> TermAlpha -> Sequent Source #

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

nullHyp :: Sequent -> Bool Source #

mkNullHyp :: TermAlpha -> Maybe Sequent Source #

mkNullHypUnsafe :: TermAlpha -> Sequent Source #

axiomOfExtensionality :: Sequent Source #

axiomOfChoice :: Sequent Source #

axiomOfInfinity :: Sequent Source #

standardAxioms :: Set Sequent Source #