Struct TVOr 

pub struct TVOr<Tag, C, Rest>(pub Tag, pub C, pub Rest);

One of the dependent family of combinators

Typically used to build linear chains of tagged unions: TVOr(0x01u8, fmt1, TVOr(0x02u8, fmt2, Uninhabited()))

Tuple Fields

0: Tag

1: C

2: Rest

Trait Implementations

impl<Tag, C, Rest> DepCombinator for TVOr<Tag, C, Rest>

where C: Consistency, Rest: DepCombinator<Key = Tag>,

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

{ Choice(Cond(key == self.0, self.1), self.2.apply(key)) }

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

{
    match value {
        Sum::Inl(_) => self.0,
        Sum::Inr(vr) => self.2.recover(vr),
    }
}

open spec fn recover_inv(&self) -> bool

{ self.2.recover_inv() }

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 = Sum<<C as Consistency>::Val, <Rest as DepCombinator>::Val>

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

type Body = Choice<Cond<C>, <Rest as DepCombinator>::Body>

The type of the body combinator produced by apply.