Structure Convert.ExpensiveConfig

Modification history

2026-09-09 20:00
Mathlib/Tactic/Convert.lean
feat: solve equalities of instances in `convert` (#40663) …
Modified Convert.ExpensiveConfigView on Github →
2026-06-17 15:42
Mathlib/Tactic/Convert.lean
feat(Convert): less aggressive congruence (#38071) …
Modified Convert.ExpensiveConfigView on Github →
2026-06-05 14:31
Mathlib/Tactic/Convert.lean
feat(Tactic): `convert` discharges side goals reducibly (#39928) …
Added Convert.ExpensiveConfigView on Github →