Struct RecursorBuilder 

pub struct RecursorBuilder {
    pub name: Name,
    pub univ_params: Vec<Name>,
    pub num_params: u32,
    pub num_indices: u32,
    pub num_motives: u32,
    pub num_minor_premises: u32,
    pub rules: Vec<RecursorRule>,
    pub is_prop: bool,
}

A builder for constructing recursor definitions programmatically.

Recursors (eliminators) are the fundamental way to consume inductive types. This builder provides a fluent API for constructing them.

Fields

name: Name

Name of the recursor (typically T.rec or T.recOn).

univ_params: Vec<Name>

Universe parameters.

num_params: u32

Number of type parameters.

num_indices: u32

Number of indices.

num_motives: u32

Number of motives (typically 1).

num_minor_premises: u32

Number of minor premises (one per constructor).

rules: Vec<RecursorRule>

Recursor rules (one per constructor).

is_prop: bool

Whether the recursor targets Prop.

Implementations

impl RecursorBuilder

pub fn new(name: Name) -> Self

Create a new builder.

pub fn univ_params(self, params: Vec<Name>) -> Self

Set universe parameters.

pub fn num_params(self, n: u32) -> Self

Set the number of parameters.

pub fn num_indices(self, n: u32) -> Self

Set the number of indices.

pub fn is_prop(self, b: bool) -> Self

Set whether the recursor targets Prop.

pub fn add_rule(self, rule: RecursorRule) -> Self

Add a recursor rule.

pub fn validate(&self) -> Result<(), String>

Validate the builder state.

Returns Ok(()) if the builder is consistent.

pub fn build_name(&self) -> Name

Return the name of the recursor.

pub fn build(&self, ty: Expr, all: Vec<Name>) -> Result<RecursorVal, String>

Build a complete RecursorVal from the builder state.

ty is the type of the recursor (must be supplied by the caller since this builder does not reconstruct the Pi telescope). all is the list of inductive type names in the mutual family.

Trait Implementations

impl Clone for RecursorBuilder

fn clone(&self) -> RecursorBuilder

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for RecursorBuilder

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

Formats the value using the given formatter.