Struct StructureEta 

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

Performs η-expansion for structure (record) types.

For a structure type S with constructor S.mk and fields f₁, f₂, …, fₙ, η-expanding an expression e : S yields:

S.mk (e.f₁) (e.f₂) … (e.fₙ)

which is definitionally equal to e by the η-rule for structures.

Implementations

impl<'a> StructureEta<'a>

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

Create a new StructureEta helper bound to the given environment.

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

Return true if ty is a Const whose name resolves in the environment to a structure-like inductive (exactly 1 constructor, 0 indices, non-recursive).

pub fn collect_field_types(&self, struct_name: &Name) -> Vec<(Name, Expr)>

Collect (field_name, field_type) pairs for the structure struct_name.

This works by looking up the unique constructor in the environment and counting num_fields from its ConstructorVal. The field types are obtained from the constructor’s type by stripping the leading Pi-binders that correspond to the inductive parameters, then collecting the remaining domain types.

Returns an empty Vec when the structure is not found.

pub fn make_proj_chain( &self, expr: &Expr, struct_name: &Name, num_fields: usize, ) -> Vec<Expr>

Build a Vec of projection expressions Proj(struct_name, i, expr) for i in 0..num_fields.

pub fn eta_expand_struct(&self, expr: &Expr, ty: &Expr) -> Option<Expr>

η-expand expr at type ty.

If ty is a structure type, returns App(… App(S.mk, proj_0(expr)) …, proj_{n-1}(expr)). Returns None when ty is not a known structure type.