Module variant 

Variant combinators

Macros

inj_ord_choice_pat

Same as above but for patterns

inj_ord_choice_result

Maps x:Ti to ord_choice_result!(T1, …, Tn)

ord_choice

This macro constructs a nested OrdChoice combinator in the form of OrdChoice(…, OrdChoice(…, OrdChoice(…, …)))

ord_choice_result

Build a type for the result of ord_choice!

ord_choice_type

Build a type for the ord_choice! macro

Structs

Choice

Combinator that tries the Fst combinator and if it fails, tries the Snd combinator.

Opt

The optional combinator that never fails. If the inner combinator fails, the result is None.

OptThen

Optional

Wrapper for the core::option::Option type. Needed because currently Verus does not implement the View trait for Option.

Enums

Either