形式化验证编程语言【免费下载链接】coqThe Rocq Prover is an interactive theorem prover, or proof assistant. 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://gitcode.com/gh_mirrors/co/coq点击查看免费下载导读本篇文章围绕 Rocq Prover原 Coq的规范语言specification language变更记录 22307-record-anon-Changed.rst 展开讲解匿名字段记录record with anonymous fields在记录构建语法{| ... |}上的行为变化现在可以在构建记录时只提供有名字段未提供的字段包括没有名字的匿名字段会自动产生待求解的洞hole而非直接报错。读完本文你将理解这一变更的语法语义、底层实现位置、测试用例证据以及它在实际开发中尤其是依赖类型类实例填充字段的场景的用法与限制。变更背景什么是匿名字段记录Rocq Prover 的记录record是带有一个构造函数的归纳类型字段是构造函数的参数。除了带名字的字段外记录还可以声明匿名字段anonymous field用_作为字段名例如Record R : { x : nat; _ : P x }.这里_ : P x是一个匿名字段它只有类型没有可引用的投影名。匿名字段不能通过投影访问也不能在记录构建语法中显式提供——因为它们根本没有名字。历史背景上匿名字段的支持由来已久在 doc/sphinx/changes.rst 中可以找到 Support of anonymous fields in record (#2555) 的记录。不过匿名字段与原始记录primitive record互斥kernel/indTyping.ml 的类型检查注释明确写着records must have 1 constructor with at least 1 argument, and no anonymous fields测试套件test-suite/output/Record.v中Record anonproj : { _ : nat }.也触发 The record anonproj could not be defined as a primitive record because it has an anonymous projection 的警告见 Record.out。变更内容详解匿名字段记录的补洞行为本次变更PR #22307作者 Gaëtan Gilbert的核心内容如下Changed:record syntax is now allowed for records with anonymous fields, producing holes for the non provided fields (anonymous fields cannot be provided since they have no name). Note that records without anonymous fields already produced holes for non provided fields instead of producing an error, so{| x : 0 |}now works to produce a value of eitherRecord R : { x : nat; y : P x }orRecord R : { x : nat; _ : P x }where previously only the former would work.翻译并拆解为三句话语法层面对含匿名字段的记录{| ... |}构建语法现在被允许使用未提供的字段会产生洞hole。语义层面匿名字段无法被显式提供因为字段没有名字未被提供的字段无论有名还是匿名都会被洞补全。行为一致性此前不含匿名字段的记录在未提供字段时已经产生洞而非报错例如Record R : { x : nat; y : P x }中省略y现在这一行为扩展到了含匿名字段的记录例如Record R : { x : nat; _ : P x }中省略匿名字段使得{| x : 0 |}对这两种记录都能构造出值而在此之前只有前者可行。变更前后的对比(* 场景一无匿名字段旧行为已支持补洞 *) Record R1 : { x : nat; y : P x }. Definition a : {| x : 0 |}. (* 旧版本即可工作y 补洞 *) (* 场景二含匿名字段本次变更新增支持 *) Record R2 : { x : nat; _ : P x }. Definition b : {| x : 0 |}. (* 旧版本报错新版本补洞 *)源码级原理补洞在内部化阶段如何实现记录构建语法的内部化internalization位于 interp/constrintern.ml 的record函数。它接收def是否带with子句和字段列表fs通过completer处理未提供的字段无with子句def Nonecompleter为每个缺失字段生成一个CHole其中的问号带有Evar_kinds.record_field信息包含field_idx与recordname见 constrintern.ml。这正是未提供的字段产生洞的实现位置——对匿名字段同样适用因为补洞只依赖字段序号与记录名不依赖字段名。有with子句def Some _需要根据字段名从def中投影出默认值若该字段没有名字则直接报错Cannot use with: this record contains anonymous fields.见 constrintern.ml。因此含匿名字段的记录不能使用with子句来继承旧值。字段补齐后代码用sort_fields ~complete:true排序并检查with子句是否被使用过若所有字段都被显式列出则报 All the fields are explicitly listed in this record: the with clause is useless.见 constrintern.ml最终组装出构造函数的应用表达式constrintern.ml。测试用例验证洞由类型类求解填补仓库的测试套件直接覆盖了本次变更。test-suite/output/Record.v的AnonField模块给出了完整场景Record.vModule AnonField. Class C (n:nat) : c {}. Record foo : { x : nat ; _ : C x }. Check {| x : 10 |}. Fail Definition bar : {| x : 10 |}. Existing Instance c. Definition bar : {| x : 10 |}. Fail Definition baz : {| bar with x : 10 |}. End AnonField.对照输出 Record.out 可以精确理解语义Check {| x : 10 |}.成功打印结果为Build_foo 10 ?c : foo其中?c : [ |- C 10]——匿名字段被补成一个待求解的洞?c。Fail Definition bar : {| x : 10 |}.在没有注册任何C 10实例时失败错误信息是 The following term contains unresolved implicit arguments: (Build_foo 10 ?c)并指出 ?c: Cannot infer 2nd field of record foo (no type class instance found)。这说明补出的洞会交给类型类求解机制去填充求解失败则构建失败。注册Existing Instance c.之后Definition bar : {| x : 10 |}.成功——洞被实例c填补。Fail Definition baz : {| bar with x : 10 |}.失败错误正是上文源码中实现的Cannot use with: this record contains anonymous fields.验证了含匿名字段记录不能用with子句这一限制。实践要点与注意事项用法含匿名字段的记录可以直接用{| 有名字段 : 值 |}构建匿名字段自动补洞补洞结果交由后续机制类型类搜索、后续evar求解填充。限制一无法显式提供匿名字段。由于没有名字{| _ : v |}这类写法不成立只能依赖补洞。限制二不可用with子句。含匿名字段的记录使用{| r with x : v |}会报Cannot use with: this record contains anonymous fields.因为继承旧值需要按字段名投影。限制三原始记录不兼容。含匿名字段的记录无法成为 primitive record参见 Record.out 的警告这与本次语法变更相互独立。典型应用匿名字段常用于承载证据字段或类型类字段如上面的_ : C x这些字段的值往往可以由类型类实例自动推导不需要用户显式给出。本次变更让这类记录可以更简洁地构建与无匿名字段时省略字段即补洞的既有行为保持一致。总结本次变更PR #22307统一了记录构建语法对省略字段的处理规则无论记录是否含匿名字段{| ... |}中未提供的字段都会产生洞而不是报错。其实现位于 interp/constrintern.ml 的record内部化逻辑测试证据见 Record.v 与 Record.out。在使用时需注意匿名字段不可显式提供、不可使用with子句这两条边界并善用类型类实例来填充由证据/类字段产生的洞。赞分享形式化验证编程语言【免费下载链接】coqThe Rocq Prover is an interactive theorem prover, or proof assistant. 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://gitcode.com/gh_mirrors/co/coq点击查看免费下载相关推荐Roc 语言取消记录可选字段name: _ 语法在记录更新与构造中的完整实现解析Roc 语言取消记录可选字段 name: _ 语法在记录更新与构造中的完整实现解析 本文以 Roc 编译器测试快照 test/snapshots/record微信/QQ/TIM 消息防撤回补丁3 分钟讲透 RevokeMsgPatcher 的用法与原理微信/QQ/TIM 消息防撤回补丁3 分钟讲透 RevokeMsgPatcher 的用法与原理 RevokeMsgPatcher 是面向 Windows 版微桌面应用即时通讯Qwen3.6-35B-A3B-Uncensored-Wasserstein-GGUF终极未审查AI模型的完整指南 Qwen3.6 35B A3B Uncensored Wasserstein GGUF终极未审查AI模型的完整指南 如果你正在寻找一款功能强大且无审查限上一篇开源字体库终极指南15款专业字体一站式获取方案下一篇如何快速获取15款专业字体开源字体库完整使用指南创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考
