def TLA.ProofMode.replacePredsAtIndices {σ : Type u} (hyps : List (NamedPred σ)) (idxs : List Nat) (preds : List (pred σ)) : List (NamedPred σ)

Replace the predicates at the given hypothesis indices.

Equations

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

def TLA.ProofMode.EntailsWithSomePredsExtractedOut {σ : Type u} (hyps : List (NamedPred σ)) (idxs : List Nat) (preds : List (pred σ)) (goal : pred σ) : Prop

An Entails goal with some hypothesis predicates extracted out for rewriting.

Equations

• TLA.ProofMode.EntailsWithSomePredsExtractedOut hyps idxs preds goal = TLA.ProofMode.Entails (TLA.ProofMode.replacePredsAtIndices hyps idxs preds) goal

def TLA.ProofMode.tlaRewrite : Lean.ParserDescr

tla_rewrite [rules] rewrites predicates in a proof-mode goal or selected proof-mode hypotheses.

With no location, it rewrites the goal predicate. For example, if the goal is q and heq : q = r, then

tla_rewrite [heq]

changes the goal to r.

Locations use Lean's location syntax, but refer to proof-mode hypotheses:

tla_rewrite [heq] at hp
tla_rewrite [← heq] at hp hq ⊢

The first rewrites only hp; the second rewrites hp, hq, and the goal. With at *, each proof-mode hypothesis and the goal are considered separately; locations that do not contain a matching occurrence are skipped as in Lean's rewrite.

Equations

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