Email Gateway (Nov 29 2024 at 09:06): Email Gateway (Nov 29 2024 at 09:06):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
Hello,
by chance I have encountered an (inconsequential) mistake in the
"Tutorial for (co)datatype definitions"
(\src\Doc\Datatypes\Datatypes.thy). The function every_snd does not do
what it promises to do (both instances). There is no recursive call!
Stepan
Email Gateway (Nov 29 2024 at 09:47):From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Dear Stepan,
Thanks for the report! It will be fixed in the next release.
If you find further errors in the (co)datatype tutorial, feel free to just drop me an email. I'm the main maintainer of that tutorial.
Best,
Jasmin
--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html
On 29. Nov 2024, at 10:06, Stepan Holub (via cl-isabelle-users Mailing List) <cl-isabelle-users@lists.cam.ac.uk> wrote:
Hello,
by chance I have encountered an (inconsequential) mistake in the "Tutorial for (co)datatype definitions" (\src\Doc\Datatypes\Datatypes.thy). The function every_snd does not do what it promises to do (both instances). There is no recursive call!
Stepan
Last updated: Jan 04 2025 at 20:18 UTC