Enum RecursionPlan 

pub enum RecursionPlan {
    IntCountdown,
    ListStructural,
    StringPosAdvance,
    MutualIntCountdown,
    MutualStringPosAdvance {
        rank: usize,
    },
    MutualSizeOfRanked {
        rank: usize,
        metric_param_index: usize,
    },
}

Proof-mode recursion support class for emitted Lean definitions.

Variants

IntCountdown

Single-function recursion where first Int parameter decreases by 1.

ListStructural

Single-function structural recursion on first List<_> parameter.

StringPosAdvance

Single-function recursion where first String stays the same and second Int parameter strictly advances (pos + k, k >= 1).

MutualIntCountdown

Mutual recursion group where first Int parameter decreases by 1 across SCC calls.

MutualStringPosAdvance

Mutual recursion group where first String is preserved and second Int either stays the same across rank-decreasing edges, or strictly advances.

Fields

rank: usize

MutualSizeOfRanked

Generic mutual recursion plan using sizeOf on a selected parameter, plus rank for same-parameter edges.

Fields

rank: usize

metric_param_index: usize

Trait Implementations

impl Clone for RecursionPlan

fn clone(&self) -> RecursionPlan

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for RecursionPlan

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

Formats the value using the given formatter.

impl PartialEq for RecursionPlan

fn eq(&self, other: &RecursionPlan) -> 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 RecursionPlan

impl Eq for RecursionPlan

impl StructuralPartialEq for RecursionPlan