Enum RecursionTree 

pub enum RecursionTree {
    Base {
        label: String,
    },
    Rec {
        label: String,
        decreasing_arg: String,
        child: Box<RecursionTree>,
    },
    Branch {
        label: String,
        arms: Vec<RecursionTree>,
    },
}

A ranked proof tree for tracking structural recursion depth.

Variants

Base

A base case (leaf).

Fields

label: String

Rec

A recursive case with a child proof tree.

Fields

label: String

decreasing_arg: String

child: Box<RecursionTree>

Branch

A branching point (e.g., match with multiple arms).

Fields

label: String

arms: Vec<RecursionTree>

Implementations

impl RecursionTree

pub fn depth(&self) -> usize

Return the maximum depth of the recursion tree.

pub fn recursive_calls(&self) -> usize

Return the number of recursive calls.

pub fn is_base(&self) -> bool

Return true if the tree is simply a base case.

Trait Implementations

impl Clone for RecursionTree

fn clone(&self) -> RecursionTree

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for RecursionTree

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

Formats the value using the given formatter.