Enum WfRelationKind 

pub enum WfRelationKind {
    Structural {
        inductive_type: Name,
        param_index: usize,
    },
    Measure {
        measure_fn: Name,
    },
    Lexicographic {
        components: Vec<WfRelationKind>,
    },
    NatSub,
    Custom {
        relation: Name,
    },
}

Well-founded relation kind for termination arguments.

Variants

Structural

Structural recursion on an inductive type.

Fields

inductive_type: Name

The inductive type being recursed on.

param_index: usize

Index of the parameter being checked.

Measure

Recursion on a numeric measure.

Fields

measure_fn: Name

The measure function.

Lexicographic

Lexicographic combination of multiple relations.

Fields

components: Vec<WfRelationKind>

The component relations.

NatSub

Well-founded recursion on natural number subtraction.

Custom

Custom user-provided well-founded relation.

Fields

relation: Name

The custom relation.

Implementations

impl WfRelationKind

pub fn is_structural(&self) -> bool

Check if this is a structural recursion.

pub fn lex_depth(&self) -> usize

Get the depth of a lexicographic argument.

pub fn description(&self) -> String

Return a human-readable description.

Trait Implementations

impl Clone for WfRelationKind

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for WfRelationKind

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

Formats the value using the given formatter.

impl Eq for WfRelationKind

impl PartialEq for WfRelationKind

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for WfRelationKind