modality_subuniv

[mikeshulman]

Is it possible to declare something as a "coercion" for purposes of not being printed, but not for purposes of being used when parsing user input? It would be nice if modality_subuniv were never printed, but when parsing user input we should first coerce a modality to a reflective subuniverse and then to a subuniverse.

[Alizter]

Here is an idea: We make a parsing only notation for modality_subuniv and deprecate it's use. That way, if it is used by a user, they will get a warning:

#[deprecated(note="We discourage coercing modalities directly to subuniverses. Please coerce to a reflective subuniverse first. ")]
Notation modality_subuniv := modality_subuniv (parsing only).

The documentation on the deprecation attribute is here: https://coq.inria.fr/refman/using/libraries/writing.html

[mikeshulman]

The problem is that even though we never write modality_subuniv explictly, it nevertheless appears sometimes in output. Would your suggestion help with this problem?

[Alizter]

I think I misunderstood you earlier then. My suggestion simply discourages users from using modality_subuniv.

You want modality_subuniv to have the printing behavior of a coercion, but not actually do any coercing? In that case, I am not aware of any mechanism to do this.

Have you got an example of where it appears in output?

Also, why don't we define Modality to extend ReflectiveSubuniverse?

[mikeshulman]

cbn makes it happen a lot. First one i found is here (put a period after the cbn to see the output).

[mikeshulman]

Also, why don't we define Modality to extend ReflectiveSubuniverse?

Because the definition of a modality that we're using doesn't include the data of a reflective subuniverse, but rather the latter can be derived from the former.