From 6d496b5113b4474b05bddd1d515306fff74e61d7 Mon Sep 17 00:00:00 2001 From: Tony Garnock-Jones Date: Wed, 15 Jun 2022 22:19:29 +0200 Subject: [PATCH] Require non-empty sequence of annotations --- cheatsheet.md | 4 ++-- preserves-binary.md | 4 +++- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/cheatsheet.md b/cheatsheet.md index e2fef67..8258997 100644 --- a/cheatsheet.md +++ b/cheatsheet.md @@ -50,7 +50,7 @@ be passed down to the decoder for the corresponding value, so that the decoder knows when to stop. **Annotations.** To annotate a `Repr` `r` (that *MUST NOT* itself -already be annotated) with some sequence of `Value`s `[v_1, ..., v_m]`, -surround `r` as follows: +already be annotated) with some sequence of `Value`s `[v_1, ..., v_m]` +(that *MUST* be non-empty), surround `r` as follows: [0xBF] ++ len(|r|) ++ r ++ len(|«v_1»|) ++ «v_1» ++...++ len(|«v_m»|) ++ «v_m» diff --git a/preserves-binary.md b/preserves-binary.md index 4f68b66..691640a 100644 --- a/preserves-binary.md +++ b/preserves-binary.md @@ -199,7 +199,9 @@ v_m]`, surround `r` as follows: [0xBF] ++ len(|r|) ++ r ++ len(|«v_1»|) ++ «v_1» ++...++ len(|«v_m»|) ++ «v_m» -The `Repr` `r` *MUST NOT* already have annotations; that is, it must not begin with `0xBF`. +The `Repr` `r` *MUST NOT* already have annotations; that is, it must not +begin with `0xBF`. The sequence `[v_1, ..., v_m]` *MUST* contain at +least one `Value`. For example, the `Repr` corresponding to textual syntax `@a@b[]`, i.e. an empty sequence annotated with two symbols, `a` and `b`, is