def Lean.Meta.Grind.isMarkedSubsingletonConst (e : Expr) : Bool

Equations

• Lean.Meta.Grind.isMarkedSubsingletonConst (Lean.Expr.const declName us) = (pure (declName == `Lean.Grind.nestedProof || declName == `Lean.Grind.nestedDecidable)).run
• Lean.Meta.Grind.isMarkedSubsingletonConst e = Id.run false

def Lean.Meta.Grind.isMarkedSubsingletonApp (e : Expr) : Bool

Equations

• Lean.Meta.Grind.isMarkedSubsingletonApp e = Lean.Meta.Grind.isMarkedSubsingletonConst e.getAppFn

def Lean.Meta.Grind.markNestedSubsingletons (e : Expr) : GrindM Expr

Wrap nested proofs and decidable instances in e with Lean.Grind.nestedProof and Lean.Grind.nestedDecidable-applications. Recall that the congruence closure module has special support for them.

Equations

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

def Lean.Meta.Grind.markProof (e : Expr) : GrindM 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 StateRefT'.run' (Lean.Meta.Grind.markNestedProof✝ e) ∅