【发布时间】：2021-10-21 08:33:02
【问题描述】：
manual 这么说
如果给定的符号字符串仅出现在打印规则中，则根本不会修改解析器。
所以我希望当我添加“仅打印”符号时，这些术语会被解析为好像没有符号一样。 但是，当我这样做时
Inductive Bit := One | Zero.
Notation "1" := One (only printing).
术语1 现在被解析为Bit
Check 1. (* 1 : Bit *)
为什么会出现这种情况？如何将1 添加为仅打印符号？
【问题讨论】：
-
这对我来说听起来像是一个错误（但我不是这方面的专家）。报告它可能是个好主意。