Cyril Cohen (Apr 12 2021 at 12:02): Cyril Cohen (Apr 12 2021 at 12:02):@Matthieu Sozeau @Arthur Charguéraud should we open a working group on the topic?
Enrico Tassi (Apr 12 2021 at 12:15):As I wrote on discourse, this reminds me of this paper https://arxiv.org/abs/1103.3320 which is using Matita's coercion system to insert Pant as a cast, and resolve the resulting unification problem via CS.
Arthur Charguéraud (Apr 12 2021 at 12:16):I'm happy to contribute on the design and the testing of this proposal.
Matthieu Sozeau (Apr 12 2021 at 12:35):Yes
Ali Caglayan (Jun 01 2021 at 11:30):I am also interested in something like this
Last updated: Apr 20 2024 at 15:01 UTC