broken link in ch13_co_inductive_types

[awalterschulze]

At the top of https://coq-community.org/coq-art/ch13_co_inductive_types/index.html

The chapter on co-inductive types of our book is mainly illustrated with the theory of finite or infinite ("lazy") lists. **This file** contains the complete development of this theory. 

This file links to https://coq-community.org/coq-art/ch13_co_inductive_types/SRC/Coinduc.v which gives a 404

[ybertot]

The file Coinduc.v is nowhere to be found in the repository. As a work around, you can use the following pointer:

https://www.labri.fr/perso/casteran/CoqArt/co-inductifs/SRC/Coinduc.v

The link wil be fixed.

[Casteran]

Hi, sorry for this error !

The real name of the file is ch13_co_inductive_types/SRC/chap13.v (on the coq-community repo). We will have to write a new README.md instead of the old index.html.

Pierre

Le 30 nov. 2020 à 09:13, Yves Bertot notifications@github.com a écrit :

The file Coinduc.v is nowhere to be found in the repository. As a work around, you can use the following pointer:

https://www.labri.fr/perso/casteran/CoqArt/co-inductifs/SRC/Coinduc.v https://www.labri.fr/perso/casteran/CoqArt/co-inductifs/SRC/Coinduc.v The link wil be fixed.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/coq-community/coq-art/issues/15#issuecomment-735628015, or unsubscribe https://github.com/notifications/unsubscribe-auth/AJW6FCUWPYOQBRKFG57JJDTSSNHZTANCNFSM4UHGBWCQ.

[awalterschulze]

No problem, just thought I'd report it, so it can be fixed for future readers. I am finding work arounds, don't worry about me.

[palmskog]

Fixed, so closing.