Theory POPLmarkRecord
theory POPLmarkRecord
imports Basis
begin
section ‹Extending the calculus with records›
text ‹
\label{sec:record-calculus}
We now describe how the calculus introduced in the previous section can
be extended with records. An important point to note is that many of the
definitions and proofs developed for the simple calculus can be reused.
›
subsection ‹Types and Terms›
text ‹
In order to represent records, we also need a type of {\it field names}.
For this purpose, we simply use the type of {\it strings}. We extend the
datatype of types of System \fsub{} by a new constructor ‹RcdT›
representing record types.
›
type_synonym name = string