Zulip Chat Archive
Stream: lean4
Topic: Lean.Name vs Lake.Name
Shreyas Srinivas (Oct 17 2023 at 22:08):
In the document page for Lean.Name, I see the type Lake.Name when defining the type of Lean.Name's constructors. Clicking on Lake.Name keeps me at Lean.Name. Are they identical?
Patrick Massot (Oct 17 2023 at 22:09):
This is a known bug.
Patrick Massot (Oct 17 2023 at 22:10):
Patrick Massot (Oct 17 2023 at 22:10):
So the answer is that you are looking at Lean.Name.
Shreyas Srinivas (Oct 17 2023 at 22:10):
ah okay. Thanks
Last updated: Dec 20 2023 at 11:08 UTC