Stream: Coq Workshop 2021

Topic: [S1T2] Porting MathComp to Hierarchy Builder


view this post on Zulip Christian Doczkal (Jul 02 2021 at 08:28):

Presentation given by @Enrico Tassi

view this post on Zulip Ben Siraphob (Jul 02 2021 at 08:51):

How much will this change affect the section on organizing theories in the math-comp book?

view this post on Zulip Christian Doczkal (Jul 02 2021 at 08:53):

Paraphrasing @Enrico Tassi

This section will have to be reworked and hopefully become simpler.

view this post on Zulip Enrico Tassi (Jul 02 2021 at 08:54):

HB can be seen as a transpiler from the high level language to what MC uses today. So the principles are the same, but the syntax is much simpler and the nasty details are hopefully hidden under the rug


Last updated: Mar 29 2024 at 10:01 UTC