Enum ConstantInfo 

pub enum ConstantInfo {
    Axiom(AxiomVal),
    Definition(DefinitionVal),
    Theorem(TheoremVal),
    Opaque(OpaqueVal),
    Inductive(InductiveVal),
    Constructor(ConstructorVal),
    Recursor(RecursorVal),
    Quotient(QuotVal),
}

Unified constant info enum (mirrors LEAN 4’s constant_info).

Every declaration in the environment is stored as a ConstantInfo. The type checker dispatches on this enum to determine reduction behavior.

Variants

Axiom(AxiomVal)

Axiom declaration.

Definition(DefinitionVal)

Definition with body.

Theorem(TheoremVal)

Theorem with proof.

Opaque(OpaqueVal)

Opaque definition.

Inductive(InductiveVal)

Inductive type.

Constructor(ConstructorVal)

Constructor of inductive type.

Recursor(RecursorVal)

Recursor (eliminator).

Quotient(QuotVal)

Quotient type component.

Implementations

impl ConstantInfo

pub fn name(&self) -> &Name

Get the name of this constant.

pub fn ty(&self) -> &Expr

Get the type of this constant.

pub fn level_params(&self) -> &[Name]

Get the universe level parameters.

pub fn common(&self) -> &ConstantVal

Get the common constant value.

pub fn is_axiom(&self) -> bool

Check if this is an axiom.

pub fn is_definition(&self) -> bool

Check if this is a definition.

pub fn is_theorem(&self) -> bool

Check if this is a theorem.

pub fn is_opaque(&self) -> bool

Check if this is opaque.

pub fn is_inductive(&self) -> bool

Check if this is an inductive type.

pub fn is_constructor(&self) -> bool

Check if this is a constructor.

pub fn is_recursor(&self) -> bool

Check if this is a recursor.

pub fn is_quotient(&self) -> bool

Check if this is a quotient component.

pub fn to_definition_val(&self) -> Option<&DefinitionVal>

Get the definition value if this is a Definition.

pub fn to_inductive_val(&self) -> Option<&InductiveVal>

Get the inductive value if this is an Inductive.

pub fn to_constructor_val(&self) -> Option<&ConstructorVal>

Get the constructor value if this is a Constructor.

pub fn to_recursor_val(&self) -> Option<&RecursorVal>

Get the recursor value if this is a Recursor.

pub fn to_quotient_val(&self) -> Option<&QuotVal>

Get the quotient value if this is a Quotient.

pub fn to_axiom_val(&self) -> Option<&AxiomVal>

Get the axiom value if this is an Axiom.

pub fn to_theorem_val(&self) -> Option<&TheoremVal>

Get the theorem value if this is a Theorem.

pub fn to_opaque_val(&self) -> Option<&OpaqueVal>

Get the opaque value if this is an Opaque.

pub fn has_value(&self, allow_opaque: bool) -> bool

Check if this constant has a computable value.

allow_opaque controls whether opaque definitions are considered.

pub fn value(&self) -> Option<&Expr>

Get the value (body/proof) if available.

pub fn reducibility_hint(&self) -> ReducibilityHint

Get the reducibility hint.

pub fn is_unsafe(&self) -> bool

Check if this declaration is unsafe.

pub fn is_structure_like(&self) -> bool

Check if this is a structure-like inductive (single constructor, not recursive).

impl ConstantInfo

pub fn kind(&self) -> ConstantKind

Return the kind of this constant.

pub fn summarize(&self) -> ConstantSummary

Build a summary of this constant.

pub fn num_level_params(&self) -> usize

Return the number of universe-level parameters.

pub fn is_polymorphic(&self) -> bool

Whether this constant is universe-polymorphic.

pub fn parent_inductive(&self) -> Option<&Name>

For constructors, return the parent inductive name.

pub fn inductive_num_params(&self) -> Option<usize>

For inductives, return the number of parameters.

pub fn inductive_num_indices(&self) -> Option<usize>

For inductives, return the number of indices.

pub fn inductive_constructors(&self) -> Option<&[Name]>

For inductives, return the list of constructor names.

pub fn ctor_num_fields(&self) -> Option<usize>

For constructors, return the number of fields.

pub fn recursor_rules(&self) -> Option<&[RecursorRule]>

For recursors, return the recursor rules.

pub fn display_string(&self) -> String

Return a display string for this constant.

Trait Implementations

impl Clone for ConstantInfo

fn clone(&self) -> ConstantInfo

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ConstantInfo

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

Formats the value using the given formatter.

impl PartialEq for ConstantInfo

fn eq(&self, other: &ConstantInfo) -> 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 ConstantInfo