Stream: Coq users

Topic: Semantics of (Strategy) Opaque on primitive projections

view this post on Zulip Paolo Giarrusso (Aug 06 2021 at 17:27):

  1. What does it mean to mark a primitive projection p as opaque — does that affect the compatibility constant or the actual primitive projection? One can mark "constants" as opaque, but apparently actual projections can be constants?
  2. Ditto for Strategy Opaque, _if_ that's a different concept. Is it? And ditto for other Strategy choices.

view this post on Zulip Paolo Giarrusso (Aug 06 2021 at 17:27):

cc @Janno

Last updated: Oct 13 2024 at 01:02 UTC