Struct InductiveTypeInfo 

pub struct InductiveTypeInfo {
    pub name: Name,
    pub num_params: u32,
    pub num_indices: u32,
    pub num_constructors: usize,
    pub is_prop: bool,
    pub is_recursive: bool,
    pub is_mutual: bool,
    pub constructor_names: Vec<Name>,
}

Summary information about an inductive type (for display/LSP use).

Fields

name: Name

Type name.

num_params: u32

Number of parameters.

num_indices: u32

Number of indices.

num_constructors: usize

Number of constructors.

is_prop: bool

Whether the type is in Prop.

is_recursive: bool

Whether the type is recursive (has recursive constructors).

is_mutual: bool

Whether the type is mutually inductive.

constructor_names: Vec<Name>

Constructor names.

Implementations

impl InductiveTypeInfo

pub fn from_type(ty: &InductiveType, is_mutual: bool) -> Self

Build info from an InductiveType.

pub fn summary(&self) -> String

Human-readable summary.

Trait Implementations

impl Clone for InductiveTypeInfo

fn clone(&self) -> InductiveTypeInfo

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for InductiveTypeInfo

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

Formats the value using the given formatter.