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).
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.
I made a draft proposition at #19029.
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.
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.
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