From d0619cb16462a9f0a3fc18917b420cc1df8f8e11 Mon Sep 17 00:00:00 2001
From: Tony Garnock-Jones <tonyg@leastfixedpoint.com>
Date: Wed, 1 Nov 2023 15:42:25 +0100
Subject: [PATCH] Correct encoding functions for trailers

---
 preserves-expressions.md | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/preserves-expressions.md b/preserves-expressions.md
index 997f036..31d390f 100644
--- a/preserves-expressions.md
+++ b/preserves-expressions.md
@@ -100,7 +100,7 @@ We write ⌜*p*⌝ for the encoding into Preserves of a P-expression *p*.
 | ⌜`,`⌝            | = | `<p |,|>`               |
 | ⌜`;`⌝            | = | `<p |;|>`               |
 | ⌜`:` ...⌝        | = | `<p |:` ...`|>`         |
-| ⌜*t*⌝            | = | ⌜*a*⌝ ... `<a>` | where *a* ... are the annotations in *t* and *t* ∈ **Trailer** |
+| ⌜*t*⌝            | = | `@`⌜*a*⌝ ... `<a>` | where `@`*a* ... are the annotations in *t* and *t* ∈ **Trailer** |
 
 The record `<a>` acts as an anchor for the annotations in a `Trailer`.
 
@@ -108,8 +108,10 @@ We overload the ⌜·⌝ notation for encoding whole `Document`s into
 sequences of Preserves values.
 
 {:.pseudocode.equations}
-| ⌜·⌝ : **P-expression Document** | ⟶ | **Preserves Sequence** |
-| ⌜*p* ...⌝                       | = | `[`⌜*p*⌝ ...`]`        |
+| ⌜·⌝ : **P-expression Document** | ⟶ | **Preserves Sequence**                    |
+| ⌜*p* ...⌝                       | = | `[`⌜*p*⌝ ...`]`                           |
+| ⌜*p* ... `@`*a* ...⌝            | = | `[`⌜*p*⌝ ... `@`⌜*a*⌝ ... `<a>]`          |
+|                                 |   | where `@`*a* ... are trailing annotations |
 
 ## <a id="reading-preserves"></a>Interpreting P-expressions as Preserves