It would be nice to have a diagnosis kind for trocq elpi predicates, like with coq-elpi's diagnosis kind.
This type would carry information about why Trocq did fail (was it a missing translation, an impossible translation).
This would allow us to further make features like etrocq or to have better error messages
It would be nice to have a diagnosis kind for trocq elpi predicates, like with coq-elpi's
diagnosiskind.This type would carry information about why Trocq did fail (was it a missing translation, an impossible translation).
This would allow us to further make features like
etrocqor to have better error messages