Struct Tag 

pub struct Tag {
    pub class: Class,
    pub constructed: bool,
    pub number: TagNumber,
}

Fields

class: Class

constructed: bool

number: TagNumber

Trait Implementations

impl ByteLen<Tag> for TagFmt

exec fn length(&self, v: &Tag) -> usize

fn exec_inv(&self) -> bool

impl Clone for Tag

fn clone(&self) -> Tag

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Tag

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl DeepView for Tag

open spec fn deep_view(&self) -> Self::V

{ *self }

type V = Tag

impl DerOrd<Tag> for TagFmt

proof fn lemma_der_serialize_len(&self, tag: Tag)

open spec fn der_remaining(&self, tag: Tag, state: TagDerState) -> Seq<u8>

{ self.spec_serialize(tag).skip(state.pos as int) }

open spec fn der_state_valid(&self, tag: Tag, state: TagDerState) -> bool

{
    &&& state.pos <= state.len
    &&& state.len <= state.bytes@.len()
    &&& state.len == self.spec_serialize(tag).len()
    &&& state.bytes@.take(state.len as int) == self.spec_serialize(tag)

}

exec fn der_start(&self, t: &Tag) -> state : TagDerState

exec fn der_next(&self, t: &Tag, state: &mut TagDerState) -> next : Option<u8>

fn der_leq(&self, left: &T, right: &T) -> bool

impl PartialEq for Tag

fn eq(&self, other: &Tag) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl PartialEqSpecImpl for Tag

fn obeys_eq_spec() -> bool

fn eq_spec(&self, other: &Self) -> bool

impl Prepare<Tag> for TagFmt

exec fn prepare(&self, v: &Tag) -> Result<usize, PreSerializeError>

fn exec_inv(&self) -> bool

impl<Output: OutputBuf> Serializer<Output, Tag> for TagFmt

exec fn serialize_into(&self, v: &Tag, obuf: &mut Output)

fn exec_inv(&self) -> bool

impl Copy for Tag

impl Eq for Tag

impl Structural for Tag

impl StructuralPartialEq for Tag