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.

partial def Lean.Elab.Tactic.Do.ProofMode.transferHypNames.collectHyps (P : Expr) (acc : List Hyp := []) : List Hyp

partial def Lean.Elab.Tactic.Do.ProofMode.transferHypNames.label (Ps : List Hyp) (P' : Expr) : MetaM (List Hyp × Expr)

def Lean.Elab.Tactic.Do.ProofMode.mFrameCore {m : Type → Type u_1} {α : Type} [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} {α : Type} [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.