pub trait Plain: Copy { }Expand description
A marker trait for types that can be extracted from snapshots in ghost code. These are type that only contain plain data and whose onership does not convey any additional information.
For example, Booleans and integers are plain, but references are not, be they
mutable or not. Indeed, the ownership of a shared reference can be used to deduce
facts, for example with PtrOwn::disjoint_lemma.
Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.