「SF-PLF」14 RecordSub

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)