Module implicit 

Dependent sequencing that omits a parsed header from the public value.

Implicit selects a body from a header like Bind, but reconstructs that header from the body during serialization.

Modules

proof

Correctness proofs for this combinator. Correctness proofs for dependent formats that omit their header value.

spec

Specification trait implementations for this combinator. Specification for dependent formats that omit their header value.

Structs

Implicit

Dependent sequential combinator with deterministic key recovery.

NBytesOf

One of the dependent family of combinators

TLVal

One of the dependent family of combinators

TVLeaf

One of the dependent family of combinators

TVOr

One of the dependent family of combinators

TagValNode

One of the dependent family of combinators

VariedLen

One of the dependent family of combinators

VoidTag

One of the dependent family of combinators

Traits

DepCombinator

A family of dependent combinators indexed by a key type.

Functions

TLVOf

TVNode

Uninhabited

VLData

VLDataOf

Type Aliases

KVFormat

Dependent family encoded by a pair of pure spec closures (apply, recover).