Commit 2021-11-30 14:25 e31b7cc4

View on Github →

chore: move run_cmd to separate file and remove comments (#111)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Mathport/Syntax.lean

deleted def Lean.Elab.Command.$(mkIdent

deleted def Lean.Elab.Command.elabIncludeCmd

deleted def Lean.Elab.Command.elabOmitCmd

deleted def Lean.Elab.Command.elabRunCmd

deleted def Lean.Elab.Term.elabCommandQuot

deleted def Lean.Parser.Term.Command.quot

Created Mathlib/Tactic/RunCmd.lean