「SF-PLF」14 RecordSub

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)