Struct InductiveFamily 

pub struct InductiveFamily {
    pub types: Vec<InductiveType>,
    pub univ_params: Vec<Name>,
}

A mutually inductive family of types.

Lean 4 supports mutual induction (e.g., Even and Odd defined together). This struct holds a group of inductive types that are checked together.

Fields

types: Vec<InductiveType>

The inductive types in the family.

univ_params: Vec<Name>

Shared universe parameters.

Implementations

impl InductiveFamily

pub fn singleton(ty: InductiveType) -> Self

Create a single-type family.

pub fn new(types: Vec<InductiveType>, univ_params: Vec<Name>) -> Self

Create a mutually inductive family.

pub fn len(&self) -> usize

Number of types in the family.

pub fn is_singleton(&self) -> bool

Whether the family contains a single type.

pub fn is_empty(&self) -> bool

Whether the family is empty.

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

All type names in the family.

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

All constructor names across all types.

pub fn find_type(&self, name: &Name) -> Option<&InductiveType>

Find a type by name.

pub fn total_constructors(&self) -> usize

Total number of constructors across all types.

Trait Implementations

impl Clone for InductiveFamily

fn clone(&self) -> InductiveFamily

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for InductiveFamily

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

Formats the value using the given formatter.