It has been 1164 days since the last update, the content of the article may be outdated.

Adding Records

coq
1
2
3
4
5
6
7
8
9
10
11
12
t ::=                          Terms:
    | {i1=t1, ..., in=tn}         record
    | t.i                         projection
    | ...

v ::=                          Values:
    | {i1=v1, ..., in=vn}         record value
    | ...

T ::=                          Types:
    | {i1:T1, ..., in:Tn}         record type
    | ...

Formalizing Records