Tutorial, distributivity improperly formulated (missing parentheses).

[flura]

https://coq.inria.fr/tutorial/1-basic-predicate-calculus End of section "1.3.3 Tauto". Retrieved at Wed May 29.

Says: Lemma distr_and : A -> B /\ C -> (A -> B) /\ (A -> C).

Should say: Lemma distr_and : (A -> B /\ C) -> (A -> B) /\ (A -> C).

Remark: Both are true and provable, but it seems to me that the former is rather trivial (A, B and C are all assumed true), while only the latter properly expresses distributivity.

[Lysxia]

For what it's worth, the tutorial is in the www repo: https://github.com/coq/www/tree/master/pages/tutorial

[Zimmi48]

FTR the HTML sources pointed to by @Lysxia are themselves generated from a LaTeX source, whose last copy is at https://github.com/coq/coq/blob/8f0e4fbc634230d89bb710547bbb50a7f959d74b/doc/tutorial/Tutorial.tex (but have since then been removed from the Coq repository). In #54, I mentioned that I personally didn't know how to generate an HTML version split over multiple pages of this LaTeX file and I that I had to split it manually. At this point, I don't even remember exactly how to generate the HTML version at all: probably using Hevea. If someone is willing to undergo this process to improve the tutorial, PRs are welcome. Otherwise, it is probably time to mark explicitly this document as "unmaintained" (it is already written that it is an "old tutorial" but this doesn't carry the same meaning).

[flura]

Unfortunately, the soon unmaintained tutorial is still the second suggestion from google if searching for "coq tutorial". Perhaps the url could be renamed (https://coq.inria.fr/tutorial/ -> https://coq.inria.fr/old-tutorial/), and a link (well visible) could be provided to the better/newer/maintained tutorials? Not very important anyway...

[Zimmi48]

Thanks for the info and the suggestion!