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)
近期评论