Struct NativeRecursor 

pub struct NativeRecursor {
    pub carrier: Term,
    pub parameters: Vec<(String, Term)>,
    pub levels: Vec<String>,
    pub ty: Term,
    pub body: Term,
}

A recursor whose motive and constructor terms retain the source container applications.

Fields

carrier: Term

The source datatype or a fully applied original container instance, open exactly over NativeRecursor::parameters.

parameters: Vec<(String, Term)>

The canonical uniform parameter telescope the carrier is open over — the telescope the recursor’s type and body abstract first. Empty for an unparameterized nested inductive.

levels: Vec<String>

Independent motive universe parameters, in motive order.

ty: Term

The recursor telescope over original carrier and constructor terms.

body: Term

The guarded implementation, checked in the original source context.