Def Lean.Elab.Command.$n:ident$[.{$us,*}]?

Modification history

2023-04-12 19:26
Mathlib/Tactic/IrreducibleDef.lean
feat: irreducible_def: support protected, equation lemmas (#3395)
Added Lean.Elab.Command.$n:ident$[.{$us,*}]?View on Github →