Commit 2022-08-13 12:14 9354f12b

View on Github →

feat: merge RunCmd and RunTac, add by_elab (#361)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Mathport/Syntax.lean

Modified Mathlib/Tactic/Conv.lean

Modified Mathlib/Tactic/RunCmd.lean

added def Mathlib.RunCmd.elabRunElab

Deleted Mathlib/Tactic/RunTac.lean

Modified scripts/nolints.json

Created test/runCmd.lean

Deleted test/runTac.lean