hello, new to lean & suspect documentation has a mistake

Stream: new members

[ast-ral]

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]

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]

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

[Eric Wieser]

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]

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]

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.