def Lean.Meta.AbstractNestedProofs.getLambdaBody (e : Expr) : Expr

def Lean.Meta.AbstractNestedProofs.isNonTrivialProof (e : Expr) : MetaM Bool

structure Lean.Meta.AbstractNestedProofs.Context : Type

• cache : Bool

@[reducible, inline]

abbrev Lean.Meta.AbstractNestedProofs.M (α : Type) : Type

partial def Lean.Meta.AbstractNestedProofs.visit (e : Expr) : M Expr

partial def Lean.Meta.AbstractNestedProofs.visit.mkAuxLemma (e : Expr) : M Expr

def Lean.Meta.abstractNestedProofs (e : Expr) (cache : Bool := true) : MetaM Expr

Replace proofs nested in e with new lemmas. The new lemmas are named using getDeclNGen.