Struct BerAnyRecBody 

pub struct BerAnyRecBody;

Trait Implementations

impl<'i> ParserRecBody<&'i [u8]> for BerAnyRecBody

Available on crate feature alloc only.

exec fn parse_body<Exec>( &self, _param: &(), Ghost(spec_rec): Ghost<ParamRecSpecs<(), Captured<AnySpec>>>, exec_rec: Exec, ibuf: &&'i [u8], ) -> PResult<CapturedAnyOwned>

where Exec: Fn(&(), &&'i [u8]) -> PResult<CapturedAnyOwned>,

type EP = ()

type O = CapturedAnyOwned

impl ProductiveRecBody for BerAnyRecBody

proof fn lemma_body_productive_inv_preservation( &self, _param: (), rec: ParamRecSpecs<(), Captured<AnySpec>>, )

impl SafeParserRecBody for BerAnyRecBody

proof fn lemma_body_safe_inv_preservation( &self, _param: (), rec: ParamRecSpecs<(), Captured<AnySpec>>, )

impl SpecRecBody for BerAnyRecBody

open spec fn spec_body( &self, _param: (), rec: ParamRecSpecs<(), Captured<AnySpec>>, ) -> Self::Body

{ ber_any_rec_body(rec) }

type Param = ()

type T = Captured<AnySpec>

type Body = Capture<Mapped<Bind<TagFmt, FnSpec<(Tag,), Sum<Bind<BerLengthFmt, FnSpec<(BerLength,), Sum<ExactLen<Tail, usize>, Sum<Repeat<(FnSpec<(Captured<AnySpec>,), bool>, FnSpec<(Captured<AnySpec>,), nat>, FnSpec<(Seq<u8>,), Option<(int, Captured<AnySpec>)>>, FnSpec<(Captured<AnySpec>,), Seq<u8>>, FnSpec<(Captured<AnySpec>, Seq<u8>), Seq<u8>>), Pair<Const<TagFmt, Tag>, Const<U8, u8>>>, Void>>>>, Void>>>, (FnSpec<((Tag, Sum<(BerLength, Sum<Seq<u8>, Sum<(Seq<Captured<AnySpec>>, (Tag, u8)), ExecNever>>), ExecNever>),), AnySpec>, FnSpec<(AnySpec,), (Tag, Sum<(BerLength, Sum<Seq<u8>, Sum<(Seq<Captured<AnySpec>>, (Tag, u8)), ExecNever>>), ExecNever>)>)>>