Stream: Coq Workshop 2021

Topic: [S2T2] À la Nelson-Oppen Combination

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

Presentation by @Frédéric Besson

view this post on Zulip Andrej Dudenhefner (Jul 02 2021 at 10:17):

Comment (not a question): I very much like the idea of congruence parameterized by injectivity lemmas.

view this post on Zulip Christian Doczkal (Jul 02 2021 at 10:19):

I second this, however this requires a mechanism to register injective functions (e.g., a type class)

Last updated: Sep 23 2023 at 15:01 UTC