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

Equations

• Lean.Meta.AbstractNestedProofs.getLambdaBody (Lean.Expr.lam binderName binderType b binderInfo) = Lean.Meta.AbstractNestedProofs.getLambdaBody b
• Lean.Meta.AbstractNestedProofs.getLambdaBody e = e

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

Equations

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

structure Lean.Meta.AbstractNestedProofs.Context : Type

• baseName : Lake.Name

structure Lean.Meta.AbstractNestedProofs.State : Type

• nextIdx : Nat

@[inline, reducible]

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

Equations

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

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

def Lean.Meta.abstractNestedProofs (mainDeclName : Lake.Name) (e : Lean.Expr) : Lean.MetaM Lean.Expr

Replace proofs nested in e with new lemmas. The new lemmas have names of the form mainDeclName.proof_

Equations

• Lean.Meta.abstractNestedProofs mainDeclName e = StateRefT'.run' (Lean.MonadCacheT.run (ReaderT.run (Lean.Meta.AbstractNestedProofs.visit e) { baseName := mainDeclName })) { nextIdx := 1 }