Zulip Chat Archive

Stream: general

Topic: punit_eq_punit


Reid Barton (Apr 23 2018 at 03:06):

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 (Apr 23 2018 at 07:54):

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.


Last updated: Dec 20 2023 at 11:08 UTC