Stream: Coq users

Topic: Disable selective literal notation

Gregory Malecha (May 17 2024 at 01:12):

I have a special string notation for names defined like this:

Declare Scope cpp_name_scope.
Delimit Scope cpp_name_scope with cpp_name.
String Notation name parse_name print_name : cpp_name_scope.
Bind Scope cpp_name_scope with name.

This is almost always the way that I want to interact with these terms, but on occasion (e.g. when I am debugging things), I want to look at the underlying syntax. Is it possible to selectively disable this printer and not other literal printers? For example, the name type contains strings and I would like to be able to disable the name printer, but still see the strings that it contains as strings.

Near solutions?

• Set Printing Raw Literals allows me to disable all literal notations, but that is too aggressive.
• I haven't found a way to disable this notation using Disable Notation.
• Beyond these, I also tried redeclaring the notation printer using:

Definition dont_print : name -> option (list Byte.byte) := fun _ => None.
Definition dont_parse : list Byte.byte -> option name := fun _ => None.

String Notation name dont_parse dont_print : cpp_name_scope.

But that didn't seem to work either. Is this possible to do in Coq? If not, is it a feature that could be added?

Notification Bot (May 17 2024 at 08:44):

This topic was moved to #Coq Notation system > Disable selective literal notation by Karl Palmskog.

Last updated: Oct 13 2024 at 01:02 UTC