Zulip Chat Archive

Stream: new members

Topic: hello, new to lean & suspect documentation has a mistake

ast-ral (Nov 07 2023 at 08:42):

Specifically, in the reference here, I think when it says so long as it does not refer to any nonrecursive arguments, it should be so long as it does not refer to any *recursive* arguments. Similarly, I believe is a telescope which does not refer to foo or any nonrecursive arguments should also say recursive arguments. Please let me know if I'm mistaken on this because I'm quite confused if what it currently says is indeed correct!

Jason Rute (Nov 07 2023 at 17:18):

Just to point out, that is a reference for Lean 3. Lean is now on Lean 4 which is significant different (especially at the level of a reference manual). There is no reference manual (yet?) for Lean 4, but there is plenty of documentation. That being said, I think how inductive works should be the same, so your question is still valid.

Jason Rute (Nov 07 2023 at 17:22):

And yes, I think you are correct. Both bullets should say “does not refer to recursive arguments”.

Eric Wieser (Nov 07 2023 at 17:43):

I think https://lean-lang.org/reference should probably be renamed to https://lean-lang.org/lean3/reference or something obvious, and the page titles changed? cc @David Thrane Christiansen, since this might be something you have the power to fix

Patrick Massot (Nov 07 2023 at 17:45):

Yes, there should be a big banner on each page of the Lean 3 reference manual saying this is about an obsolete version of Lean, hopefully with a link to an updated version.

ast-ral (Nov 07 2023 at 23:50):

Excellent, thank you for double checking that for me! Thanks as well for pointing out the documentation was out of date, I found it through a search engine so I had no clue that it wasn't current. Will stick to sources from the page you linked in the future.

Last updated: Dec 20 2023 at 11:08 UTC