Coq如何设置记录类型指定字段仅解析、美化打印时隐藏

实现方式 #

你要求的「myProof字段支持解析、美化打印时自动隐藏」的需求无法直接在记录声明阶段通过原生语法配置，需要通过额外命令实现，有两种常用方案可选：

方案1：通过Arguments命令设置隐式参数（最简方案） #

在你的记录定义后追加一行Arguments配置即可：

Record myRec : Type := {
  myNat : nat;
  myProof : myNat > 0
}.
(* 将构造器的第二个证明参数标记为隐式 *)
Arguments Build_myRec _ {_}.

配置后Coq打印myRec类型的实例时会自动隐藏证明字段，你编写代码时仍然可以正常传入myProof字段的值，也可以用@Build_myRec的语法显式展示传入证明参数。

方案2：通过Notation搭配only printing修饰符实现（自定义程度更高） #

如果需要完全自定义记录的打印格式，可以用仅打印生效的记号实现：

(* 仅在美化打印时生效的自定义格式，解析阶段不识别该记号 *)
Notation "{| myNat := n |}" := (Build_myRec n _) (only printing, format "{| 'myNat' := n |}").

该方案不会影响代码解析逻辑，你写代码时仍然需要按完整语法传入myProof字段，打印时会自动替换为你定义的精简格式。

选型建议 #

如果仅需要隐藏证明字段，优先选方案1，无需额外维护记号规则；如果需要定制整个记录的打印展示样式，选方案2灵活性更高。

内容的提问来源于stack exchange，提问作者Bob