def Lean.Elab.Tactic.Do.ProofMode.mRevert {m : Type → Type u} [Monad m] [MonadLiftT MetaM m] (goal : MGoal) (ref : TSyntax `ident) (k : MGoal → m Expr) : m Expr

Equations

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

def Lean.Elab.Tactic.Do.ProofMode.mRevertForallN {m : Type → Type u} [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (n : Nat) (hypName : Name) (k : MGoal → m Expr) : m Expr

Turn goal hᵢ : Hᵢ ⊢ₛ T e₁ ... eₙ into hᵢ : fun sₙ ... s₁ => Hᵢ h : fun sₙ ... s₁ => ⌜s₁ = e₁ ∧ ... ∧ sₙ = eₙ⌝ ⊢ₛ T

Equations

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

def Lean.Elab.Tactic.Do.ProofMode.elabMRevert : Tactic

Equations

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