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)
☛兄dei，请我喝杯茶☚
