Struct VoidTag 

pub struct VoidTag<Tag>(pub PhantomData<Tag>);

One of the dependent family of combinators

Typically used in the “uninhabited” branch of a TVOr chain.

Tuple Fields

0: PhantomData<Tag>

Trait Implementations

impl<Tag> DepCombinator for VoidTag<Tag>

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

{ Void("Impossible") }

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

{
    use vstd::pervasive::arbitrary;
    arbitrary::<Tag>()
}

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

type Key = Tag

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

type Val = ExecNever

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

type Body = Void

The type of the body combinator produced by apply.

fn recover_inv(&self) -> bool