search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.66k stars 632 forks source link

Make it possible to enable/disable a `String Notation` #19043

Open gmalecha opened 2 weeks ago

gmalecha commented 2 weeks ago

Is your feature request related to a problem?

Currently, regular notations can be enabled and disabled selectively using Disable Notation, but there is no way to do this with String Notation and Number Notation.

Proposed solution

The nicest solution would be to extend the Disable Notation mechanism to support string notations. This seems like it could be done by adding an additional table that tracks whether each string notation is enabled or not.

Wild speculation This table would need to be consulted in uninterp_prim_token to filter the list from prim_token_uninterp_infos. I have not looked into the parsing side.

Alternative solutions

An alternative solution is to make it so that registering an overlapping String Notation overwrites the previous notation. To me, this makes sense as the semantics anyways, but using it for this case requires that you know the name of the parsing/printing function.

Additional context

Additional context here: https://coq.zulipchat.com/#narrow/stream/423352-Coq-Notation-system/topic/Disable.20selective.20literal.20notation