Def Mathlib.evalExtractLet

Modification history

2024-03-15 22:49
Mathlib/Tactic/ExtractLets.lean
chore: fix `extract_lets` without `at` (#11400) …
Deleted Mathlib.evalExtractLetView on Github →
2023-06-29 02:25
Mathlib/Tactic/ExtractLets.lean
feat: `extract_lets` tactic (#3897) …
Added Mathlib.evalExtractLetView on Github →