Commit 2021-11-29 17:58 561e9d63

View on Github →

feat: irreducible_def: universe levels, equations (#109) This brings the syntax closer to def and should make it easier to use it in mathport.

Estimated changes

Modified Mathlib/Tactic/IrreducibleDef.lean

deleted theorem Lean.Elab.Command.$n_def

added theorem Lean.Elab.Command.$n_def:ident

added structure Lean.Elab.Command.Wrapper$[.{$us,*}]?

deleted structure Lean.Elab.Command.Wrapper

added def Lean.Elab.Command.definition$[.{$us,*}]?

deleted def Lean.Elab.Command.definition

Modified test/irreducibleDef.lean