Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Wrap nested proofs e
with Lean.Grind.nestedProof
-applications.
Recall that the congruence closure module has special support for Lean.Grind.nestedProof
.
Instances For
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