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

Equations

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

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

Equations

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

def Lean.Meta.Grind.markNestedProofs (e : Expr) : MetaM 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_3 e

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

Given a proof e, mark it with Lean.Grind.nestedProof

Equations

• Lean.Meta.Grind.markProof e = if e.isAppOf `Lean.Grind.nestedProof = true then pure e else Lean.Meta.Grind.markProof.unsafe_impl_3 e