Stream: math-comp users

Topic: "An Introduction to Small-Scale Reflection in Coq"


view this post on Zulip Patrick Nicodemus (May 23 2022 at 12:00):

I am reading the book "An Introduction to Small-Scale Reflection in Coq" by Gonthier and Mahboubi.

Are there solutions to the exercises available anywhere? It says the solutions were hosted at http://www.msr-inria.inria.fr/Projects/math-components/ but this link is dead.

view this post on Zulip Karl Palmskog (May 23 2022 at 12:02):

have you checked here? https://github.com/math-comp/tutorial_material

view this post on Zulip Patrick Nicodemus (May 23 2022 at 12:04):

Oh this is nice! But it doesn't seem to be what I want

view this post on Zulip Karl Palmskog (May 23 2022 at 13:47):

ideally the files from here should be added to the repo, unless they are fundamentally broken: https://web.archive.org/web/20121215131540/http://www.msr-inria.inria.fr/Projects/math-components/ (e.g., this file)

view this post on Zulip Patrick Nicodemus (May 25 2022 at 08:24):

Karl Palmskog said:

ideally the files from here should be added to the repo, unless they are fundamentally broken: https://web.archive.org/web/20121215131540/http://www.msr-inria.inria.fr/Projects/math-components/ (e.g., this file)

The first file works for me, haven't checked the others yet

view this post on Zulip Laurent Théry (Jun 01 2022 at 12:08):

@Patrick Nicodemus Assia tutorial has been added to https://github.com/math-comp/tutorial_material

view this post on Zulip Patrick Nicodemus (Jun 03 2022 at 02:30):

Thank you very much!


Last updated: Jan 29 2023 at 18:03 UTC