Commit 2022-07-27 13:58 876d9cc4

View on Github →

feat: add inhabit tactic (#340)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Mathport/Syntax.lean

Created Mathlib/Tactic/Inhabit.lean

added def Lean.Elab.Tactic.evalInhabit

added def Lean.Elab.Tactic.nonempty_prop_to_inhabited

Created test/Inhabit.lean