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: Aug 11 2022 at 03:02 UTC