Trait DeepViewIdentity 

pub trait DeepViewIdentity: DeepView<V = Self> + Copy {
    // Required method
    proof fn lemma_deep_view_identity(&self);
}

Executable values whose deep view is the value itself.

ASN.1 DEFAULT needs this law to make its executable equality test line up with the spec-level decision to omit the field. Generated ENUMERATED value types implement it.

Required Methods

proof fn lemma_deep_view_identity(&self)

ensures

self.deep_view() == *self,

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.

Implementations on Foreign Types

impl DeepViewIdentity for bool

proof fn lemma_deep_view_identity(&self)

impl DeepViewIdentity for i8

proof fn lemma_deep_view_identity(&self)

impl DeepViewIdentity for i16

proof fn lemma_deep_view_identity(&self)

impl DeepViewIdentity for u8

proof fn lemma_deep_view_identity(&self)

Implementors

impl DeepViewIdentity for UtcTime