punit_eq_punit

Stream: general

[Reid Barton]

This definition (from library/init/data/punit.lean) is less general than probably intended because () is (apparently) built-in notation for unit.star only, and so the full inferred type is actually punit_eq_punit : ∀ (a : punit.{1}), @eq.{1} punit.{1} a unit.star.

lemma punit_eq_punit (a : punit) : a = () :=
punit_eq a ()

Since this is in the core Lean library, is there any hope to change it?

[Patrick Massot]

Since this is in the core Lean library, is there any hope to change it?

Someone should really read that Zulip bot documentation. Programming a bot to detect this question and answer "no" is probably a nice exercise then.