Hi. In elpi/coq-lib.elpi, coq.term->gref
has a last clause that calls fatal-error-w-data
, which breaks what I am currently trying to do since I want to do different things depending on whether my term has a gref head or not. I temporarily added a copy of coq.term->gref
that fails silently to proceed with my work, but I am curious to know why this design was chosen (if this is not already documented somewhere) and if there is a standard workaround that does not involve changing coq-elpi's code.
I think both predicates have a place, the one asserting and the one checking (hence failing).
Usually a->b
are conversions which do not fail (unless the programmer misuses them).
I'm pretty sure we have term-is-gref?
in HB or maybe in TC. The addition to coq-lib would be welcome.
Oh, I see, it is in HB, thanks. I guess the whole content of HB/common/stdpp.elpi is meant to be ported back to coq-elpi, does it not?
@Quentin VERMANDE see https://coq.zulipchat.com/#narrow/stream/253928-Elpi-users-.26-devs/topic/.E2.9C.94.20Grafting.20in.20an.20implication/near/397540505
You can add
pred do-not-fail.
:before "term->gref:fail"
coq.term->gref _ _ :- do-not-fail, !, false.
and then call do-not-fail => coq.term->gref X Y
.
This also work, but is for black belts ;-)
Yes, the stdpp code should be merged back at some point.
Oh, excellent, thanks. If you think I can, I may try to do something about the merging.
Last updated: Oct 13 2024 at 01:02 UTC