Mathlib Changelog
v4
Changelog
About
Github
Def
Lean.Elab.Command.elabIncludeCmd
Modification history
2021-11-30 14:25
Mathlib/Mathport/Syntax.lean
chore: move run_cmd to separate file and remove comments (#111)
Deleted
Lean.Elab.Command.elabIncludeCmd
View on Github →
2021-11-08 09:32
Mathlib/Mathport/Syntax.lean
refactor(Mathport): move mathport prelude to mathlib4 (#80) …
Added
Lean.Elab.Command.elabIncludeCmd
View on Github →