theorem TLA.ProofMode.Entails_or_left {σ : Type u} {hyps : List (NamedPred σ)} {a b : pred σ} : Entails hyps a → Entails hyps [tlafml|a ∨ b]

theorem TLA.ProofMode.Entails_or_right {σ : Type u} {hyps : List (NamedPred σ)} {a b : pred σ} : Entails hyps b → Entails hyps [tlafml|a ∨ b]

def TLA.ProofMode.tacticTlaLeft : Lean.ParserDescr

tlaLeft reduces a disjunctive proof-mode goal p ∨ q to its left disjunct p.

Equations

• TLA.ProofMode.tacticTlaLeft = Lean.ParserDescr.node `TLA.ProofMode.tacticTlaLeft 1024 (Lean.ParserDescr.nonReservedSymbol "tlaLeft" false)

def TLA.ProofMode.tacticTlaRight : Lean.ParserDescr

tlaRight reduces a disjunctive proof-mode goal p ∨ q to its right disjunct q.

Equations

• TLA.ProofMode.tacticTlaRight = Lean.ParserDescr.node `TLA.ProofMode.tacticTlaRight 1024 (Lean.ParserDescr.nonReservedSymbol "tlaRight" false)