Struct NBytesOf 

pub struct NBytesOf<Len, Then>(pub PhantomData<Len>, pub Then);

One of the dependent family of combinators

Typically used as Implicit(U16Le, NBytesOf(inner_fmt)).

Tuple Fields

0: PhantomData<Len>

1: Then

Trait Implementations

impl<Len, Then> DepCombinator for NBytesOf<Len, Then>

where Len: AsLen, Then: SpecByteLen + Consistency<Val = Then::T>,

open spec fn apply(&self, key: Self::Key) -> Self::Body

{ ExactLen(key, self.1) }

open spec fn recover(&self, value: Self::Val) -> Self::Key

{ Len::as_self(self.1.byte_len(value)) }

proof fn lemma_recover_consistent(&self, key: Self::Key, value: Self::Val)

type Key = Len

The type of keys parsed by the head combinator/to be recovered during serialization.

type Val = <Then as Consistency>::Val

The type of values consumed/produced by the body combinator.

type Body = ExactLen<Then, Len>

The type of the body combinator produced by apply.

fn recover_inv(&self) -> bool