Def Lean.Elab.Tactic.nonempty_prop_to_inhabited

Modification history

2022-07-27 13:58
Mathlib/Tactic/Inhabit.lean
feat: add inhabit tactic (#340)
Added Lean.Elab.Tactic.nonempty_prop_to_inhabitedView on Github →