Theorem Lean.Elab.Command.$n_def

Modification history

2021-11-29 17:58
Mathlib/Tactic/IrreducibleDef.lean
feat: irreducible_def: universe levels, equations (#109) …
Deleted Lean.Elab.Command.$n_defView on Github →
2021-11-22 09:47
Mathlib/Tactic/IrreducibleDef.lean
feat: add irreducible_def command (#99)
Added Lean.Elab.Command.$n_defView on Github →