Stream: Coq users

Topic: bypass_check(guard) in section


view this post on Zulip Ali Caglayan (Feb 08 2023 at 21:01):

Why can't I #[bypass_check(guard)] inside a section? Is the ability to skip the guard condition not handled by cooking?

view this post on Zulip Ali Caglayan (Feb 08 2023 at 21:02):

Specifically I get an error message like this:

Changing typing flags inside sections is not allowed.

view this post on Zulip Gaëtan Gilbert (Feb 08 2023 at 21:39):

because the typing flags are attached to definitions, so the typing flags used to check the variables would get lost
see https://github.com/coq/coq/issues/14317

view this post on Zulip Pierre-Marie Pédrot (Feb 10 2023 at 07:52):

FTR attaching this flag to the definition is broken because it breaks SR (e.g. through module inline).

view this post on Zulip Pierre-Marie Pédrot (Feb 10 2023 at 07:52):

I have a beginning of patch where this data is attached to the (co)fixpoints instead, which is semantically much better behaved.


Last updated: Jun 25 2024 at 19:01 UTC