Struct LexOrder 

pub struct LexOrder {
    pub components: Vec<String>,
}

A combinator for building lexicographic well-founded orderings.

Fields

components: Vec<String>

Component measure names in decreasing priority.

Implementations

impl LexOrder

pub fn new(components: Vec<impl Into<String>>) -> Self

Construct from a list of measure component names.

pub fn push(self, component: impl Into<String>) -> Self

Add an additional (lowest-priority) component.

pub fn arity(&self) -> usize

Return the number of components.

pub fn type_string(&self) -> String

Describe the lex order as a tuple type string.

pub fn check_decrease( &self, values_before: &[u64], values_after: &[u64], ) -> bool

Verify that a concrete sequence of (before, after) pairs is lexicographically decreasing using the given values for each component.

values_before[i] and values_after[i] are u64 values of component i.

Trait Implementations

impl Clone for LexOrder

fn clone(&self) -> LexOrder

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for LexOrder

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.