Struct SingletonKReducer 

pub struct SingletonKReducer<'a> { /* private fields */ }

Performs K-like reduction on singleton types.

A singleton type (in OxiLean’s sense) is an inductive type with

• exactly 1 constructor, and
• 0 non-parameter fields.

All elements of a singleton type are definitionally equal to the unique constructor (applied only to its uniform parameters). This enables a restricted form of the K axiom: pattern matching on self-equality can be simplified because any proof of a = a must equal rfl.

Implementations

impl<'a> SingletonKReducer<'a>

pub fn new(env: &'a Environment) -> Self

Create a new SingletonKReducer bound to the given environment.

pub fn is_singleton_type(&self, ty: &Expr) -> bool

Return true when ty (looked up as a Const head) has exactly 1 constructor with 0 non-parameter fields.

pub fn get_unique_ctor(&self, type_name: &Name) -> Option<Name>

Return the unique constructor name for type_name if it is a singleton.

pub fn k_reduce(&self, _expr: &Expr, ty: &Expr) -> Option<Expr>

K-reduce expr : ty.

For a singleton type the canonical element is the unique zero-field constructor constant. Returns Some(canonical) when applicable, None otherwise.

pub fn apply_k_reduction(motive: &Expr, proof: &Expr) -> Option<Expr>

Attempt to simplify Rec(motive, proof) on a singleton type.

When both motive and proof involve a singleton type, the match can be eliminated because proof must equal the canonical constructor. Returns Some(simplified) when a simplification is found.