Mathlib Changelog
v4
Changelog
About
Github
Def
elabTermWithoutNewMVars
Modification history
2025-10-14 16:26
Mathlib/Util/ElabWithoutMVars.lean
feat(Tactic/Order): frontend for `order` (#27066) …
Added
elabTermWithoutNewMVars
View on Github →