Struct TerminationProof 

pub struct TerminationProof {
    pub function_name: String,
    pub ordering: String,
    pub verified: bool,
}

Well-founded induction certificate proving termination.

Fields

function_name: String

The function name.

ordering: String

The well-founded ordering used.

verified: bool

Whether the termination argument has been fully verified.

Implementations

impl TerminationProof

pub fn new( function_name: impl Into<String>, ordering: impl Into<String>, ) -> Self

Create a termination proof by a given ordering.

pub fn verify(&mut self)

Mark the termination proof as verified.

Trait Implementations

impl Clone for TerminationProof

fn clone(&self) -> TerminationProof

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TerminationProof

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

Formats the value using the given formatter.