Equations
- Lean.Meta.AbstractNestedProofs.getLambdaBody (Lean.Expr.lam binderName binderType b binderInfo) = Lean.Meta.AbstractNestedProofs.getLambdaBody b
- Lean.Meta.AbstractNestedProofs.getLambdaBody e = e
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
Equations
Instances For
Replace proofs nested in e
with new lemmas. The new lemmas are named using getDeclNGen
.
Equations
- Lean.Meta.abstractNestedProofs e cache = do let __do_lift ← Lean.Meta.isProof e if __do_lift = true then pure e else (ReaderT.run (Lean.Meta.AbstractNestedProofs.visit e) { cache := cache }).run