Enum TerminationStrategy 

pub enum TerminationStrategy {
    Structural,
    Measure,
    Lexicographic,
    WellFounded,
    Mutual,
}

Heuristic for choosing a termination proof strategy.

Variants

Structural

Recurse on structurally smaller arguments.

Measure

Use an explicit numeric measure function.

Lexicographic

Use a lexicographic tuple of measures.

WellFounded

Use a well-founded relation other than <.

Mutual

Multiple-argument mutual recursion.

Implementations

impl TerminationStrategy

pub fn description(self) -> &'static str

Return a description of the strategy.

pub fn all() -> &'static [TerminationStrategy]

Return all available strategies.

Trait Implementations

impl Clone for TerminationStrategy

fn clone(&self) -> TerminationStrategy

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TerminationStrategy

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

Formats the value using the given formatter.

impl PartialEq for TerminationStrategy

fn eq(&self, other: &TerminationStrategy) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for TerminationStrategy

impl Eq for TerminationStrategy

impl StructuralPartialEq for TerminationStrategy