Def Mathlib.RunCmd.elabRunElab

Modification history

2024-03-05 04:47
Mathlib/Tactic/RunCmd.lean
chore: move Mathlib to v4.7.0-rc1 (#11162) …
Deleted Mathlib.RunCmd.elabRunElabView on Github →
2022-10-20 15:23
Mathlib/Tactic/RunCmd.lean
chore: update lean + std4 10-20 (#483)
Modified Mathlib.RunCmd.elabRunElabView on Github →
2022-08-13 12:14
Mathlib/Tactic/RunCmd.lean
feat: merge RunCmd and RunTac, add `by_elab` (#361)
Added Mathlib.RunCmd.elabRunElabView on Github →