source
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

Instances For

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

- Lean.Meta.Grind.isMarkedSubsingletonApp e = (Lean.Meta.Grind.isMarkedSubsingletonConst e.getAppFn && e.getAppNumArgs == 2)

Instances For

source
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.

Instances For

source
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) ∅

Instances For