Stream: Coq users

Topic: Unfolding prim projections requires `beta` — intended?


view this post on Zulip Paolo Giarrusso (Aug 30 2021 at 12:33):

It seems that, to unfold primitive projection foo (I don't mean the wrapper), I need progress cbv beta delta [foo] not just progress cbv delta [foo]. Is that expected? I do realize this matches the behavior for usual projections, since those are wrappers over lambdas.

view this post on Zulip Pierre-Marie Pédrot (Aug 30 2021 at 12:36):

This is https://github.com/coq/coq/commit/978ae7d9323558099efb0c4e4e39549221378d5d

view this post on Zulip Pierre-Marie Pédrot (Aug 30 2021 at 12:37):

IMHO this is an anti-feature but it's too late to fix this kind of code without wreaking havoc...

view this post on Zulip Paolo Giarrusso (Aug 30 2021 at 13:40):

Makes sense, thanks!

view this post on Zulip Paolo Giarrusso (Aug 30 2021 at 14:29):

and the new behavior should be part of a larger redesign such as https://github.com/coq/ceps/pull/57.


Last updated: Jan 29 2023 at 03:28 UTC