Struct DetailedTerminationResult 

pub struct DetailedTerminationResult {
    pub terminates: bool,
    pub wf_relation: Option<WfRelationKind>,
    pub function_name: Name,
    pub explanation: String,
    pub recursive_calls: Vec<RecCallInfo>,
}

Result of a termination check with detailed information.

Fields

terminates: bool

Whether termination was verified.

wf_relation: Option<WfRelationKind>

The well-founded relation used (if termination was verified).

function_name: Name

The function name.

explanation: String

Explanation of why termination was/wasn’t verified.

recursive_calls: Vec<RecCallInfo>

All recursive calls found.

Implementations

impl DetailedTerminationResult

pub fn non_recursive(name: Name) -> Self

Create a termination result for a non-recursive function.

pub fn success(name: Name, wf: WfRelationKind, calls: Vec<RecCallInfo>) -> Self

Create a successful termination result.

pub fn failure( name: Name, calls: Vec<RecCallInfo>, reason: impl Into<String>, ) -> Self

Create a failure result.

Trait Implementations

impl Clone for DetailedTerminationResult

fn clone(&self) -> DetailedTerminationResult

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for DetailedTerminationResult

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

Formats the value using the given formatter.