Def Mathlib.Command.Variable.completeBinders

Modification history

2023-06-21 19:20
Mathlib/Tactic/Variable.lean
feat: `variable?` command for automatically adding typeclass dependencies (#3162) …
Added Mathlib.Command.Variable.completeBindersView on Github →