no multi-defn boxes

diff --git a/ralf/_posts/2018-04-05-a-formal-look-at-pinning.md b/ralf/_posts/2018-04-05-a-formal-look-at-pinning.md
index 4aed608945629e1ac8b10b4659ee213fc7aabfe8..98e0477cf1a3f252c8eee937887cecccd4407ec2 100644 (file)
--- a/ralf/_posts/2018-04-05-a-formal-look-at-pinning.md
+++ b/ralf/_posts/2018-04-05-a-formal-look-at-pinning.md
@@ -154,6 +154,8 @@ Formally:
 ```
 Box<T>.own(bytes) := exists |ptr, inner_bytes| bytes.try_into() == Ok(ptr) &&
   ptr.points_to_owned(inner_bytes) && T.own(inner_bytes)
 ```
 Box<T>.own(bytes) := exists |ptr, inner_bytes| bytes.try_into() == Ok(ptr) &&
   ptr.points_to_owned(inner_bytes) && T.own(inner_bytes)

+```
+```

 (&'a mut T).own(bytes) := exists |ptr| bytes.try_into() == Ok(ptr) &&
   borrowed('a,
     exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes))
 (&'a mut T).own(bytes) := exists |ptr| bytes.try_into() == Ok(ptr) &&
   borrowed('a,
     exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes))


@@ -166,6 +168,8 @@ This could look as follows:
 ```
 Box<T>.own(ptr: Pointer) :=
   exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes)
 ```
 Box<T>.own(ptr: Pointer) :=
   exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes)

+```
+```

 (&'a mut T).own(ptr: Pointer) :=
   borrowed('a, exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes))
 ```
 (&'a mut T).own(ptr: Pointer) :=
   borrowed('a, exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes))
 ```


@@ -223,6 +227,8 @@ A list of bytes makes a valid `PinBox<T>` if those bytes form a pointer `ptr` su
 For `Pin<'a, T>`, `ptr` is valid if we have borrowed `T.pin(ptr)` for lifetime `'a`.
 ```
 PinBox<T>.own(ptr) := T.pin(ptr)
 For `Pin<'a, T>`, `ptr` is valid if we have borrowed `T.pin(ptr)` for lifetime `'a`.
 ```
 PinBox<T>.own(ptr) := T.pin(ptr)

+```
+```

 Pin<'a, T>.own(ptr) := borrowed('a, T.pin(ptr))
 ```
 
 Pin<'a, T>.own(ptr) := borrowed('a, T.pin(ptr))
 ```