Enum TerminationEvidence 

pub enum TerminationEvidence {
    Structural {
        arg_index: u32,
    },
    Lexicographic {
        measures: Vec<String>,
    },
    Unknown,
}

Abstract termination evidence: witness for why a function terminates.

Variants

Structural

Structural recursion on argument idx.

Fields

arg_index: u32

Lexicographic

Lexicographic tuple ordering.

Fields

measures: Vec<String>

Unknown

Unknown; may not terminate.

Implementations

impl TerminationEvidence

pub fn is_proven(&self) -> bool

Return whether termination is proven.

pub fn describe(&self) -> String

Format a description.

Trait Implementations

impl Clone for TerminationEvidence

fn clone(&self) -> TerminationEvidence

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TerminationEvidence

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

Formats the value using the given formatter.