Skip to main content

Module refined

vest_lib::combinators

Module refined

Expand description

Predicate refinement and constant-value formats.

Refined keeps only values satisfying a predicate. Const fixes that value and is commonly used for static tags or discriminants.

Modules§

exec: Executable trait implementations for this combinator. Executable predicates and refined-format implementations.
proof: Correctness proofs for this combinator. Correctness proofs for predicates, refinements, and constants.
spec: Specification trait implementations for this combinator. Specifications for predicates, refinements, and constants.

Structs§

Const: Constant-value combinator: matches a specific constant value.
PrefixTagged: Sugar for Preceded { a: Const(inner, tag), a_val: tag, b: body }.
Refined: Value refinement combinator: filters values through a predicate.
SuffixTagged: Sugar for Terminated { a: body, b: Const(inner, tag), b_val: tag }.