unsafe def Lean.Meta.Grind.markNestedProofsImpl (e : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• Lean.Meta.Grind.markNestedProofsImpl e = (Lean.Meta.Grind.markNestedProofsImpl.visit e).run' Lean.mkPtrMap

unsafe def Lean.Meta.Grind.markNestedProofsImpl.visit (e : Lean.Expr) : StateRefT' IO.RealWorld (Lean.PtrMap Lean.Expr Lean.Expr) Lean.MetaM Lean.Expr

Equations

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

def Lean.Meta.Grind.markNestedProofs (e : Lean.Expr) : Lean.MetaM Lean.Expr

Wrap nested proofs e with Lean.Grind.nestedProof-applications. Recall that the congruence closure module has special support for Lean.Grind.nestedProof.

Equations

• Lean.Meta.Grind.markNestedProofs e = Lean.Meta.Grind.markNestedProofs.unsafe_impl_1 e