Def Lean.Elab.mkSelectInsertParamsInstanceHandler

Modification history

2023-10-05 03:08
Mathlib/Tactic/Widget/SelectInsertParamsClass.lean
feat: Select and insert widgets (#7260) …
Added Lean.Elab.mkSelectInsertParamsInstanceHandlerView on Github →