「SF-PLF」14 RecordSub

零式的天空

发布于 2022-03-02 09:41:55

39100

代码可运行

文章被收录于专栏：零域Blog零域Blog

运行总次数：0

代码可运行

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)

本文参与腾讯云自媒体同步曝光计划，分享自作者个人站点/博客。

原始发表：2021-03-28，如有侵权请联系 cloudcommunity@tencent.com 删除

本文分享自作者个人站点/博客前往查看

如有侵权，请联系 cloudcommunity@tencent.com 删除。

本文参与腾讯云自媒体同步曝光计划，欢迎热爱写作的你一起参与！

登录后参与评论

0 条评论

热度