The Erased struct witnesses the logical ownership of a value of type T while remaining zero-sized. This can be used for ghost proofs of soundness.


The Exists trait is intended to be used with impl, to denote an argument where the existence of a value is sufficient as an argument

A type T implements SingleThread if at any time there is a single thread from which all values/references to values of this type may be accessed.

This trait denotes a type which has at most one logical identity at all times. This is sufficient to make borrowing decisions based only on the type, without regards to value identity.