Theorem Lean.Elab.Command.$n_def:ident

Modification history

2023-04-12 19:26
Mathlib/Tactic/IrreducibleDef.lean
feat: irreducible_def: support protected, equation lemmas (#3395)
Deleted Lean.Elab.Command.$n_def:identView on Github →
2021-11-29 17:58
Mathlib/Tactic/IrreducibleDef.lean
feat: irreducible_def: universe levels, equations (#109) …
Added Lean.Elab.Command.$n_def:identView on Github →