Module recursive 

Bounded fixpoint combinator for recursive and mutually recursive formats.

Body proof traits state preservation of each invariant under the inductive hypothesis.

Re-exports

pub use exec::ParserRecBody;

pub use exec::PrepareRecBody;

pub use exec::SerializerRecBody;

pub use proof::EquivSerializersGeneralRecBody;

pub use proof::NoLookAheadRecBody;

pub use proof::NonMalleableRecBody;

pub use proof::SPRoundTripDpsRecBody;

pub use proof::StrictRecBody;

pub use spec::BundledSpecs;

pub use spec::GoodSerializerRecBody;

pub use spec::NonTailFmtRecBody;

pub use spec::ParamRecSpecs;

pub use spec::ProductiveRecBody;

pub use spec::SafeParserRecBody;

pub use spec::SoundParserRecBody;

pub use spec::SpecRecBody;

Modules

exec

Executable trait implementations for this combinator. Executable interfaces for bounded recursive format bodies.

proof

Correctness proofs for this combinator. Correctness proofs and recursive-body preservation helpers for super::FixWith.

spec

Specification trait implementations for this combinator. Fixpoint specifications and recursive-body interfaces.

Structs

FixWith

Bounded fixpoint combinator for parameterized recursive formats.