diff --git a/docs/user-guide/src/syntax.md b/docs/user-guide/src/syntax.md
index f102e468c3a..ce4682d6ec2 100644
--- a/docs/user-guide/src/syntax.md
+++ b/docs/user-guide/src/syntax.md
@@ -6,6 +6,7 @@ Prusti specifications are a superset of Rust boolean expressions. They must be d
| --- | --- |
| [`old(...)`](#old-expressions) | Value of expression in a previous state |
| [`... ==> ...`](#implications) | Implication |
+| [`... === ...`](#snapshot-equality) | Snapshot equality |
| [`forall(...)`](#quantifiers) | Universal quantifier |
| [`exists(...)`](#quantifiers) | Existential quantifier |
| [... |= ...
](#specification-entailments) | Specification entailment |
@@ -14,7 +15,7 @@ Prusti specifications are a superset of Rust boolean expressions. They must be d
Old expressions are used to refer to the value that a memory location pointed at by a mutable reference had at the beginning of the function:
-```rust
+```rust,noplaypen
use prusti_contracts::*;
#[ensures(*x == old(*x) + 1)]
@@ -27,7 +28,7 @@ pub fn inc(x: &mut u32) {
Implications express a [relationship](https://en.wikipedia.org/wiki/Material_conditional) between two boolean expressions:
-```rust
+```rust,noplaypen
#[pure]
#[ensures(result ==> self.len() == 0)]
#[ensures(!result ==> self.len() > 0)]
@@ -36,17 +37,41 @@ pub fn is_empty(&self) -> bool;
There is no syntax for logical equivalences ("if and only if"), because this coincides with `==`:
-```rust
+```rust,noplaypen
#[pure]
#[ensures(result == (self.len() == 0))]
pub fn is_empty(&self) -> bool;
```
+## Snapshot Equality
+
+Snapshot equality (`===`) compares the
+[snapshots](https://viperproject.github.io/prusti-dev/dev-guide/encoding/types-snap.html)
+of two values; essentially checking if the two values are structurally equal. In
+contrast, the standard equality (`==`) between values is determined by the
+implementation of
+[`PartialEq`](https://doc.rust-lang.org/std/cmp/trait.PartialEq.html). These two
+equalities do not necessarily coincide. For example, some types do not implement
+`PartialEq`, or their implementation cannot be encoded as a pure function.
+Nonetheless, snapshot equality could be used to compare values of such types, as
+in the following code:
+
+```rust,noplaypen
+#[requires(a === b)]
+fn foo(a: T, b: T) {}
+
+struct X { a: i32 }
+
+fn main() {
+ foo(X { a: 1 }, X { a: 1 });
+}
+```
+
## Quantifiers
Quantifiers are typically used for describing how a method call changes a container such as a vector:
-```rust
+```rust,noplaypen
#[requires(0 <= index && index < self.len())]
#[ensures(self.len() == old(self.len()))]
#[ensures(self.lookup(index) == value)]