Struct VariedLen 

pub struct VariedLen<Len = u8>(pub PhantomData<Len>);

One of the dependent family of combinators

Typically used as Implicit(U8, VLData()).

Tuple Fields

0: PhantomData<Len>

Trait Implementations

impl<Len: AsLen> DepCombinator for VariedLen<Len>

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

{ Varied(key) }

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

{ Len::as_self(value.len()) }

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 = Seq<u8>

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

type Body = Varied<Len>

The type of the body combinator produced by apply.

fn recover_inv(&self) -> bool