Stream: Coq devs & plugin devs

Topic: A sealed/unsealed attribute


view this post on Zulip Hugo Herbelin (May 15 2024 at 07:35):

I'm tempted by experimenting adding a sealed attribute soon (as in CEP #42). Noone already tried, correct?

Internally, this "attribute" is already called opaque. A priori, I'm going to keep this internal name.

A priori, I'm going to add it to the Declare.Info.t data (with a default value depending on the name of the declaration).

view this post on Zulip Hugo Herbelin (May 15 2024 at 09:13):

Also, what about passing a DefAttributes.t to most of functions interpreting a declaration (like do_fixpoint, do_definition, etc.? That would make the code more compact and at the same time ensure that all possible attributes are well taken into account.

view this post on Zulip Hugo Herbelin (May 17 2024 at 15:47):

I made a draft proposition at #19029.

view this post on Zulip Hugo Herbelin (May 17 2024 at 15:53):

I'm realizing that some attributes are about individual components of a mutual definition, e.g. clearbody, or opacity or user_warns or locality, or canonical_instance (and maybe also reversible) though some others not, like polymorphic, using, typing_flags, program. What do you think? Should we allow a syntax of the following form:

#[clearbody]
Fixpoint f n := match n with 0 => 0 | S n => g n end
#[clearbody]
with g n := match n with 0 => 0 | S n => f n end.

Not a big deal if all components should share the same value but just wondering.

view this post on Zulip Théo Zimmermann (May 17 2024 at 16:11):

Yes, it would make sense to accept attributes that are more fine-grained than the command name. (This is already supported in record definitions IIRC.) But your example is not immediately readable to me. I wonder if it isn't because of a sort of parenthesis problem. I would rather expect something like:

Fixpoint
#[clearbody] f n := match n with 0 => 0 | S n => g n end
with
#[clearbody] g n := match n with 0 => 0 | S n => f n end.

view this post on Zulip Hugo Herbelin (May 17 2024 at 16:17):

Oh, you mean having attributes applying to the whole block before Fixpoint and the ones applying to individual components after. That's a good idea.


Last updated: Oct 13 2024 at 01:02 UTC