theorem TLA.ProofMode.Entails_drop_hyps {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} (subHyps : List (NamedPred σ)) (hinc : List.map NamedPred.pred subHyps ⊆ List.map NamedPred.pred hyps) : Entails subHyps goal → Entails hyps goal

theorem TLA.ProofMode.Entails_clear {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} (toClear : List String) : Entails (List.filter (fun (h : NamedPred σ) => !toClear.contains h.name) hyps) goal → Entails hyps goal

theorem TLA.ProofMode.Entails_clear_except {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} (toKeep : List String) : Entails (List.filter (fun (h : NamedPred σ) => toKeep.contains h.name) hyps) goal → Entails hyps goal

def TLA.ProofMode.tlaClearExceptTac : Lean.ParserDescr

tla_clear h₁ h₂ ... removes temporal hypotheses from the proof-mode context. The target predicate is unchanged, but the remaining proof must not use the cleared hypotheses.

For example, from a context containing hp : p, hq : q, and goal q,

tla_clear hp

leaves only hq : q in the proof-mode context.

Extensions:

• tla_clear * - h₁ h₂ ... removes every temporal hypothesis except the named ones. The kept hypotheses stay in their original order. For example, from hp : p, hq : q, hr : r,

  tla_clear * - hq
  

  leaves only hq : q.

Equations

• One or more equations did not get rendered due to their size.

def TLA.ProofMode.tlaClearTac : Lean.ParserDescr

tla_clear h₁ h₂ ... removes temporal hypotheses from the proof-mode context. The target predicate is unchanged, but the remaining proof must not use the cleared hypotheses.

For example, from a context containing hp : p, hq : q, and goal q,

tla_clear hp

leaves only hq : q in the proof-mode context.

Extensions:

• tla_clear * - h₁ h₂ ... removes every temporal hypothesis except the named ones. The kept hypotheses stay in their original order. For example, from hp : p, hq : q, hr : r,

  tla_clear * - hq
  

  leaves only hq : q.

Equations

• One or more equations did not get rendered due to their size.

def TLA.ProofMode.clearTacDSimps : Array Lean.Name

Reduction rules used after clearing a proof-mode hypothesis.

Equations

• TLA.ProofMode.clearTacDSimps = #[`List.filter, `List.contains, `List.elem, `Bool.or, `Bool.and, `Bool.not, `String.reduceBEq, `String.reduceBNe, `Bool.false_or, `Bool.or_false]

def TLA.ProofMode.tlaClearByName (name : List String) : Lean.Elab.Tactic.TacticM Unit

Clear the proof-mode hypotheses with the given names.

Equations

• One or more equations did not get rendered due to their size.