Struct InductiveType 

pub struct InductiveType {
    pub name: Name,
    pub univ_params: Vec<Name>,
    pub num_params: u32,
    pub num_indices: u32,
    pub ty: Expr,
    pub intro_rules: Vec<IntroRule>,
    pub recursor: Name,
    pub is_nested: bool,
    pub is_prop: bool,
}

An inductive type declaration.

Fields

name: Name

Type name

univ_params: Vec<Name>

Universe parameters

num_params: u32

Number of parameters (non-varying arguments)

num_indices: u32

Number of indices (varying arguments)

ty: Expr

Type of the inductive type (Pi type over params and indices)

intro_rules: Vec<IntroRule>

Introduction rules (constructors)

recursor: Name

Recursor name (generated automatically)

is_nested: bool

Whether this is a nested inductive type

is_prop: bool

Whether this type is in Prop (proof-irrelevant)

Implementations

impl InductiveType

pub fn new( name: Name, univ_params: Vec<Name>, num_params: u32, num_indices: u32, ty: Expr, intro_rules: Vec<IntroRule>, ) -> Self

Create a new inductive type.

pub fn arity(&self) -> u32

Get the arity (total number of arguments).

pub fn is_recursive(&self) -> bool

Check if this inductive type is recursive.

pub fn constructor_names(&self) -> Vec<&Name>

Return a vector of references to constructor names.

pub fn num_constructors(&self) -> usize

Return the number of constructors.

pub fn to_constant_infos( &self, ) -> Result<(ConstantInfo, Vec<ConstantInfo>, ConstantInfo), KernelError>

Generate ConstantInfo declarations for this inductive type.

Returns: (InductiveVal, Vec<ConstructorVal>, RecursorVal).

The recursor is derived by the kernel derivation machinery (crate::inductive::derive) following Lean 4’s inductive.cpp: minor premises carry induction hypotheses, the elimination universe and K flag are computed from the declared type (the caller-supplied is_prop flag is ignored), and rule right-hand sides are closed lambdas over params ++ motives ++ minors ++ fields.

This environment-free path performs no positivity or universe checking; use crate::inductive::derive::add_inductive_family for the checked path.

Trait Implementations

impl Clone for InductiveType

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 InductiveType

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

Formats the value using the given formatter.

impl PartialEq for InductiveType

fn eq(&self, other: &Self) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for InductiveType