Struct AuxMap 

pub struct AuxMap {
    pub aux_type: Name,
    pub container: Name,
    pub container_levels: Vec<Level>,
    pub params: Vec<Expr>,
    pub aux_ctors: Vec<(Name, Name)>,
    pub aux_rec: Name,
    pub container_rec: Name,
}

How one auxiliary inductive maps back to the real container it specializes. Retained through derivation so S3 restoration can substitute the auxiliary type / constructors / recursor back to the real container constants and drop the abstracted parameters.

Fields

aux_type: Name

The fresh auxiliary inductive type name (e.g. T._nested_0).

container: Name

The real container type-former it specializes (e.g. List).

container_levels: Vec<Level>

The container’s universe-level arguments at the nested occurrence.

params: Vec<Expr>

The concrete arguments As the container was specialized at (the abstracted parameters restoration must re-insert / drop).

aux_ctors: Vec<(Name, Name)>

(auxiliary ctor name, real container ctor name) in declaration order.

aux_rec: Name

The auxiliary recursor name the kernel will derive (<aux_type>.rec).

container_rec: Name

The real container’s recursor name (<container>.rec).

Trait Implementations

impl Clone for AuxMap

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 AuxMap

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

Formats the value using the given formatter.