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, ) -> (ConstantInfo, Vec<ConstantInfo>, ConstantInfo)

Generate ConstantInfo declarations for this inductive type.

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

Trait Implementations

impl Clone for InductiveType

fn clone(&self) -> InductiveType

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: &InductiveType) -> bool

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for InductiveType