Stream: Coq devs & plugin devs

Topic: (Primitive) Projections and local defs in CClosure (whd)

view this post on Zulip Janno (Jan 12 2021 at 11:32):

I am observing a difference between Definitions and posed variables and (primitive?) projections when reducing them using CClosure.whd_val with CClosure.RedFlags.red_add_transparent CClosure.all TransparentState.full. With a Definition the term my_projection my_definition reduces just fine. With a posed variable the projection is stuck. Is this intentional? Am I using the wrong flags to reduce this term?

view this post on Zulip Janno (Jan 12 2021 at 11:36):

Another data point: lazy reduces the projection applied to the posed variable.

Last updated: Sep 15 2024 at 13:02 UTC