Struct InductiveMember 

pub struct InductiveMember {
    pub name: String,
    pub params: Vec<(String, Term)>,
    pub sort: Term,
    pub constructors: Vec<(String, Term)>,
    pub full_constructors: bool,
}

One member of an Command::InductiveBlock.

The shape is the legacy Command::Inductive’s: the parameters are split out and bound by name, and sort is the DECLARED arity after the parameters — its binders are the indices and its final sort is the universe the type lives in; it refers to a parameter as the global of that name.

A constructor is written one of two ways, the same for every constructor of a member:

• full_constructors == false — C : T, where T omits the parameter prefix and refers to a parameter as the global of its name; the registration puts the member’s parameters back;
• full_constructors == true — C (p₁ : T₁) … (pₙ : Tₙ) : T, the constructor RESTATING its parameter telescope, and constructors holds each FULL type, parameters bound as ordinary binders. The restated types may spell a parameter differently from the member (Lean’s HAdd.mk binds γ : outParam (Type w) where HAdd’s arity says Type w); the kernel’s block door checks them and registers the constructor exactly as written. A member with no parameters has one form only, and the flag is false.

Fields

name: String

params: Vec<(String, Term)>

sort: Term

constructors: Vec<(String, Term)>

full_constructors: bool

Trait Implementations

impl Clone for InductiveMember

fn clone(&self) -> InductiveMember

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for InductiveMember

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

Formats the value using the given formatter.