Enum ProofStep 

pub enum ProofStep {
    Beta {
        redex_depth: u32,
    },
    Delta {
        name: String,
    },
    Zeta,
    Iota {
        recursor: String,
        ctor_idx: u32,
    },
    Eta,
    SubstLevel {
        params: Vec<String>,
    },
    Assumption,
}

A single step in a proof reduction sequence.

These steps record the high-level reduction moves taken during kernel type-checking, enabling efficient replay or auditing.

Variants

Beta

β-reduction: substitute the argument into the body.

redex_depth records the nesting depth at which this reduction occurred.

Fields

redex_depth: u32

De Bruijn depth of the beta-redex site.

Delta

δ-reduction: unfold a named definition.

Fields

name: String

Name of the definition that was unfolded.

Zeta

ζ-reduction: substitute a let-binding.

Iota

ι-reduction: reduce a recursor application to a branch.

Fields

recursor: String

Name of the recursor that fired.

ctor_idx: u32

Index of the constructor branch selected.

Eta

η-reduction: contract λ x, f x to f.

SubstLevel

Universe-level substitution.

Fields

params: Vec<String>

Parameter names substituted.

Assumption

Appeal to a local assumption (hypothesis) in the context.

Trait Implementations

impl Clone for ProofStep

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 ProofStep

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

Formats the value using the given formatter.

impl Display for ProofStep

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

Formats the value using the given formatter.

impl Eq for ProofStep

impl PartialEq for ProofStep

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for ProofStep