Struct ProofNormalizer 

pub struct ProofNormalizer;

A minimal proof normalizer that applies beta reduction to proof terms.

In the kernel, proof terms are normalised before definitional equality checks to avoid spurious inequality due to un-reduced redexes.

Implementations

impl ProofNormalizer

pub fn beta_reduce(term: &Expr) -> Expr

Beta-reduce a proof term to its normal form.

This is a simple structural pass that eliminates (fun x => body) arg redexes by substituting arg for bound variable 0 in body.

pub fn subst_bvar(term: Expr, depth: u32, replacement: &Expr) -> Expr

Substitute replacement for bound variable depth in term.

This implements the standard capture-avoiding substitution for de Bruijn terms.

pub fn count_redexes(term: &Expr) -> usize

Count the number of beta-redexes remaining in a term.

pub fn is_beta_normal(term: &Expr) -> bool

Returns true if the term is already in beta-normal form (no redexes).