Def Lean.Elab.Command.definition

Modification history

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