为什么Coq的only printing记号会修改解析器？如何正确设置仅打印记号

问题原因 #

你遇到的与手册描述不一致的情况，本质是数字字面量的特殊处理逻辑和普通自定义记号不同：

• Coq官方手册中关于only printing规则不会修改解析器的描述，针对的是普通自定义语法记号（比如自定义二元运算符、特殊前缀语法等）。而数字、字符串属于内置特殊字面量，有独立的解析、打印适配体系，不受普通记号规则的完全约束。
• 你最初的定义没有给1的记号指定专属作用域，默认注册到了全局作用域。此时哪怕标注了only printing，Coq的数字解析推导逻辑也会将这个1到One的映射纳入类型推导候选，所以无上下文的Check 1会优先匹配到最近注册的这个映射，返回Bit类型的结果。

解决方法 #

要实现仅打印1、不修改原有解析逻辑的需求，将该记号绑定到Bit类型专属的局部作用域即可，参考实现代码：

Inductive Bit := One | Zero.

(* 声明Bit类型专属作用域 *)
Declare Scope bit_scope.
(* 将Bit类型与该作用域绑定，所有Bit类型的术语默认使用该作用域的打印规则 *)
Bind Scope bit_scope with Bit.
(* 仅在bit_scope下定义数字的仅打印规则 *)
Notation "1" := One (only printing) : bit_scope.
Notation "0" := Zero (only printing) : bit_scope.

效果验证 #

• 全局作用域下执行Check 1.仍返回1 : nat，原有解析逻辑完全没有被修改
• 执行Check One.会打印1 : Bit，符合仅打印的需求
• 即使手动打开bit_scope，输入1仍然会被解析为nat类型，不会触发Bit的映射，完全符合only printing的预期。

内容的提问来源于stack exchange，提问作者Proof-By-Sledgehammer