Punit docstring typo?

Stream: lean4

[Bhavik Mehta]

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]

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]

Is a Lean4 PR to fix this welcome?

[Sebastian Ullrich]

Yes, doc fixes are generally welcome