@Matthieu Sozeau @Arthur Charguéraud should we open a working group on the topic?
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.
I'm happy to contribute on the design and the testing of this proposal.
I am also interested in something like this
Last updated: Oct 21 2021 at 20:02 UTC