「软件基础 - PLF」 14. Subtyping with Records

Posted by Hux on March 14, 2019
1
2
3
4
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)