Zulip Chat Archive

Stream: lean4

Topic: Punit docstring typo?


Bhavik Mehta (Jul 09 2021 at 16:47):

The docstring for Unit here in Prelude mentions that Unit is an abbreviation for PUnit.{0}, but Unit : Sort 1, so it should be an abbreviation for PUnit.{1}, I'm pretty sure. The same thing appears in Lean 3, where I presume this docstring essentially came from.

Mac (Jul 09 2021 at 17:00):

Yeah, I noticed that as well and was curious if it was mistaken. I didn't have the initiative to ask about it , though. Still, I am curious what the answer is.

Bhavik Mehta (Jul 12 2021 at 19:44):

Is a Lean4 PR to fix this welcome?

Sebastian Ullrich (Jul 12 2021 at 20:19):

Yes, doc fixes are generally welcome


Last updated: Dec 20 2023 at 11:08 UTC