def Lean.Meta.abstractProof {m : Type → Type} [Monad m] [MonadLiftT MetaM m] [MonadEnv m] [MonadOptions m] [MonadFinally m] (proof : Expr) (cache : Bool := true) (postprocessType : Expr → m Expr := pure) : m Expr

Abstracts the given proof into an auxiliary theorem, suitably pre-processing its type.

Equations

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

def Lean.Meta.AbstractNestedProofs.getLambdaBody (e : Expr) : 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 : Expr) : MetaM Bool

Equations

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

structure Lean.Meta.AbstractNestedProofs.Context : Type

• cache : Bool

@[reducible, inline]

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

Equations

• Lean.Meta.AbstractNestedProofs.M = ReaderT Lean.Meta.AbstractNestedProofs.Context (Lean.MonadCacheT Lean.ExprStructEq Lean.Expr Lean.MetaM)

partial def Lean.Meta.AbstractNestedProofs.visit (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.

Equations

• Lean.Meta.abstractNestedProofs e cache = do let __do_lift ← Lean.Meta.isProof e if __do_lift = true then pure e else (ReaderT.run (Lean.Meta.AbstractNestedProofs.visit e) { cache := cache }).run