Module sequence 

Sequencing combinators

Structs

Pair

Combinator that sequentially applies two combinators, where the second combinator depends on the first one.

Preceded

Combinator that sequentially applies two combinators and returns the result of the second one.

Terminated

Combinator that sequentially applies two combinators and returns the result of the first one.

Enums

POrSType

A type that can be either a PType or an SType, whose View is the same as PType. This is used for the continuation in Pair.

Traits

Continuation

Use this Continuation trait instead of Fn(Input) -> Output to avoid unsupported Verus features

Type Aliases

GhostFn

Alias for Verus’s spec function type.

SpecPair

Alias for a spec dependent pair combinator.