document snapshot equality (viperproject#1137)

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 |
 | [<code>... &#x7C;= ...</code>](#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<T>(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)]