From d9f20370eb5fcb94dd2ada55ebba44d4c3d38953 Mon Sep 17 00:00:00 2001
From: James Clark <jjc@jclark.com>
Date: Tue, 12 May 2020 16:29:35 +0700
Subject: [PATCH] Allow readonly fields in record type descriptor

Fixes #464.
---
 lang/spec.html | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/lang/spec.html b/lang/spec.html
index 158fafc6..023685a1 100644
--- a/lang/spec.html
+++ b/lang/spec.html
@@ -1534,6 +1534,12 @@ <h5>Record types</h5>
 optional field.</li>
 </ul>
 <p>
+If an <code>individual-field-descriptor</code> specifies <code>readonly</code>,
+then there is also a constraint that the field has its read-only bit set.
+Furthermore, the type of the field is the intersection of <code>readonly</code>
+and the type specified by the type-descriptor.
+</p>
+<p>
 The order of the <code>individual-field-descriptor</code>s within a
 <code>record-type-descriptor</code> is not significant. Note that the delimited
 identifier syntax allows the field name to be any non-empty string.
@@ -1567,6 +1573,12 @@ <h5>Record types</h5>
 <em>closed</em>.
 </p>
 <p>
+If a record type descriptor is closed and every individual-type-descriptor
+specifies <code>readonly</code>, then it describes a type that is a subtype of
+<code>readonly</code>: a shape belongs to the type only if its read-only bit is
+set.
+</p>
+<p>
 A <code>default-value</code> specifies a default value for the field, which is
 used when the record type descriptor is used to construct a mapping value but no
 value is specified explicitly for the field. The type descriptor contains a