Is it possible to use a term (and not a definition) as a coercion? I have an interface like:
Module M.
Record t : Set := mk { is_const : bool ; frac : Qp }.
Notation c := (mk false).
Notation m := (mk true).
End M.
And I want to declare
Coercion (M.mk false) : Qp >-> M.t.
I can make a definition for M.mk false
but then syntactic pattern matching does not work.
it is not possible
How difficult would it be to implement something like that?
I think we generally don't like to store data as terms rather than in a constant, because then we have to deal with questions about universes in a adhoc way, the term doesn't get checked by the kernel etc
maybe we could have a way to make coercions as "to be reduced when inserted"?
also omitting such coercions when printing (regardless of if they're registered as terms or if they're reduced when inserted) would be difficult and probably not worth the effort
having a way to reduce coercions when they are inserted would solve my problem. Personally, I don't care if the coercion is printed, and it seems reasonable to have different behavior if the coercion is a term or unfolded upon insertion
thanks for your feedback
"Arguments your_def /." might be a decent approximation: "your_def" would be unfolded by simpl/cbn :-)
Recently I've been advocating for a variation of Arguments def /
for which unfolding is performed eagerly (a bit like eta is after some tactics).
would def
be autounfolded in definitions that use it after elaboration? (Unfolded and beta-reduced I guess, without touching other redexes)
Last updated: Mar 28 2024 at 11:01 UTC