Commit 2024-11-03 18:36 872dd564

View on Github →

chore: move #help to Batteries (batteries#969) (#17257)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/Common.lean

Deleted Mathlib/Tactic/HelpCmd.lean

Deleted test/help_cmd.lean

deleted def foo