Def elabTermWithoutNewMVars

Modification history

2025-10-14 16:26
Mathlib/Util/ElabWithoutMVars.lean
feat(Tactic/Order): frontend for `order` (#27066) …
Added elabTermWithoutNewMVarsView on Github →