Inductive ty : Type :=
(* record types *)
| RNil : ty
| RCons : string → ty → ty → ty.
we need typecon to identify record…
```coq Inductive tm : Type := | rproj …? isn’t it as well? (* record terms *) | rnil : tm | rcons : string → tm → tm → tm. ``
as a list…
for Record, can compiler reorder the fields? (SML and OCaml)
读者怎么说
先看读者反馈，再直接在当前页面继续讨论。不用绑定社交账号，填个昵称、抓一只娃娃就能留言。
快捷身份
留下你的想法
选一个预设身份，或者直接填昵称；写完点发布，抓到指定的娃娃就能提交。若显示“需要配置 Waline”，说明站点还缺少可写评论后端。
当前未选择预设身份