def Lean.Elab.Tactic.Do.ProofMode.transferHypNames (P P' : Expr) : MetaM Expr

If P' is a conjunction of unnamed hypotheses that are a subset of the named hypotheses of P, transfer the names of the hypotheses of P to the hypotheses of P'.

Equations

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

def Lean.Elab.Tactic.Do.ProofMode.mFrameCore {m : Type → Type u_1} [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (kFail : m Expr) (kSuccess : Expr → Expr → MGoal → m Expr) : m Expr

Equations

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

def Lean.Elab.Tactic.Do.ProofMode.mTryFrame {m : Type → Type u_1} [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (k : MGoal → m Expr) : m Expr

Equations

• Lean.Elab.Tactic.Do.ProofMode.mTryFrame goal k = Lean.Elab.Tactic.Do.ProofMode.mFrameCore goal (k goal) fun (x x : Lean.Expr) (goal : Lean.Elab.Tactic.Do.ProofMode.MGoal) => k goal

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

Equations

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