Require non-empty sequence of annotations

This commit is contained in:
Tony Garnock-Jones 2022-06-15 22:19:29 +02:00
parent 6138bfdb8a
commit 6d496b5113
2 changed files with 5 additions and 3 deletions

View File

@ -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»

View File

@ -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