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

Modification history

2023-04-12 19:26
Mathlib/Tactic/IrreducibleDef.lean
feat: irreducible_def: support protected, equation lemmas (#3395)
Deleted Lean.Elab.Command.definition$[.{$us,*}]?View on Github →
2021-11-29 17:58
Mathlib/Tactic/IrreducibleDef.lean
feat: irreducible_def: universe levels, equations (#109) …
Added Lean.Elab.Command.definition$[.{$us,*}]?View on Github →