Struct Environment 

pub struct Environment { /* private fields */ }

The global environment containing all checked declarations.

Implementations

impl Environment

pub fn add_quot(&mut self) -> Result<(), EnvError>

Install the four #QUOT primitives (Quot, Quot.mk, Quot.lift, Quot.ind) with their canonical, kernel-constructed types.

This is the trusted #QUOT entry point, mirroring Lean’s add_quot in src/kernel/quot.cpp:

• Precondition: Eq must already exist as an inductive of the expected shape (one constructor Eq.refl), because Quot.lift’s soundness hypothesis mentions Eq. A typed error is returned otherwise.
• All four types are constructed in-kernel (universe-polymorphic in u, plus v for Quot.lift); the caller never supplies them.
• The four constants are added atomically. If any name already exists, nothing is installed.
• A once-only Environment::quot_initialized flag is set; a second add_quot is a typed error, and any other ConstantInfo::Quotient addition is rejected by Environment::add_constant.

impl Environment

pub fn new() -> Self

Create a new empty environment.

pub fn add(&mut self, decl: Declaration) -> Result<(), EnvError>

Add a legacy declaration to the environment.

Returns an error if a declaration with the same name already exists.

pub fn add_constant(&mut self, ci: ConstantInfo) -> Result<(), EnvError>

Add a ConstantInfo to the environment.

Quotient constants (ConstantInfo::Quotient) are rejected here: the four #QUOT primitives may only be installed atomically through Environment::add_quot, which constructs their canonical types in-kernel. This prevents a caller from smuggling a Quotient entry with an arbitrary (possibly unsound) type past the checker.

pub fn quot_initialized(&self) -> bool

Whether the four #QUOT primitives have been installed.

pub fn get(&self, name: &Name) -> Option<&Declaration>

Look up a legacy declaration by name.

pub fn find(&self, name: &Name) -> Option<&ConstantInfo>

Look up a constant info by name.

pub fn contains(&self, name: &Name) -> bool

Check if a declaration exists.

pub fn len(&self) -> usize

Get the number of declarations.

pub fn is_empty(&self) -> bool

Check if the environment is empty.

pub fn get_defn(&self, name: &Name) -> Option<(Expr, ReducibilityHint)>

Get a definition’s value and hint (for reduction).

pub fn is_inductive(&self, name: &Name) -> bool

Check if a name refers to an inductive type.

pub fn is_constructor(&self, name: &Name) -> bool

Check if a name refers to a constructor.

pub fn is_recursor(&self, name: &Name) -> bool

Check if a name refers to a recursor.

pub fn is_quotient(&self, name: &Name) -> bool

Check if a name refers to a quotient.

pub fn is_structure_like(&self, name: &Name) -> bool

Check if a name refers to a structure-like inductive.

pub fn get_inductive_val(&self, name: &Name) -> Option<&InductiveVal>

Get the inductive type info for a name.

pub fn get_constructor_val(&self, name: &Name) -> Option<&ConstructorVal>

Get the constructor info for a name.

pub fn get_recursor_val(&self, name: &Name) -> Option<&RecursorVal>

Get the recursor info for a name.

pub fn get_quotient_val(&self, name: &Name) -> Option<&QuotVal>

Get the quotient info for a name.

pub fn get_type(&self, name: &Name) -> Option<&Expr>

Get the type of a constant (from ConstantInfo).

pub fn get_level_params(&self, name: &Name) -> Option<&[Name]>

Get the universe level parameters for a constant.

pub fn instantiate_const_type( &self, name: &Name, levels: &[Level], ) -> Option<Expr>

Instantiate a constant’s type with universe levels.

pub fn constant_names(&self) -> impl Iterator<Item = &Name>

Iterate over all constant names.

pub fn constant_infos(&self) -> impl Iterator<Item = (&Name, &ConstantInfo)>

Iterate over all constant infos.

Trait Implementations

impl Clone for Environment

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Environment

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

Formats the value using the given formatter.

impl Default for Environment

fn default() -> Self

Returns the “default value” for a type.