Enum RecursionPlan 

pub enum RecursionPlan {
    IntCountdown {
        param_index: usize,
    },
    IntAscending {
        param_index: usize,
        bound_lean: String,
    },
    LinearRecurrence2,
    ListStructural {
        param_index: usize,
    },
    SizeOfStructural,
    StringPosAdvance,
    MutualIntCountdown,
    MutualStringPosAdvance {
        rank: usize,
    },
    MutualSizeOfRanked {
        rank: usize,
    },
}

Proof-mode recursion support class for emitted Lean definitions.

Variants

IntCountdown

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

Fields

param_index: usize

IntAscending

Single-function recursion where an Int parameter increases by 1 up to a bound. bound_lean is the Lean expression of the upper bound (e.g. 8 or xs.length).

Fields

param_index: usize

bound_lean: String

LinearRecurrence2

Single-function recurrence with n < 0 guard, 0/1 bases, and a linear second-order recurrence over previous results, emitted through a private Nat helper.

ListStructural

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

Fields

param_index: usize

SizeOfStructural

Single-function structural recursion on a recursive user-defined type 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 structural parameters, plus rank for same-measure edges.

Fields

rank: 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 Eq for RecursionPlan

impl StructuralPartialEq for RecursionPlan