Def Mathlib.evalExtractLets

Modification history

2024-03-15 22:49
Mathlib/Tactic/ExtractLets.lean
chore: fix `extract_lets` without `at` (#11400) …
Added Mathlib.evalExtractLetsView on Github →