Environment extension for the forward-reasoning part of the gcongr
tactic #
An extension for gcongr_forward
.
- eval : Lean.Expr → Lean.MVarId → Lean.MetaM Unit
Read a gcongr_forward
extension from a declaration of the right type.
Equations
- One or more equations did not get rendered due to their size.
Environment extensions for gcongrForward
declarations