Commit 2021-11-22 09:47 978ee9f0

View on Github →

feat: add irreducible_def command (#99)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Tactic/IrreducibleDef.lean

added theorem Lean.Elab.Command.$n_def

added structure Lean.Elab.Command.Wrapper

added def Lean.Elab.Command.definition

Created test/irreducibleDef.lean