Def Mathlib.Command.Variable.ignorevariable?

Modification history

2025-11-19 06:07

Mathlib/Tactic/Variable.lean

chore: move Mathlib to the module system (#31786) …

Modified Mathlib.Command.Variable.ignorevariable?View on Github →

2023-06-21 19:20

Mathlib/Tactic/Variable.lean

feat: `variable?` command for automatically adding typeclass dependencies (#3162) …

Added Mathlib.Command.Variable.ignorevariable?View on Github →