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 the inductive type the primitives assume — one universe parameter, the type {α : Sort u} → α → α → Prop, and one constructor of type {α : Sort u} → (a : α) → @Eq α a a (check_eq_present) — 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 add_constants(&mut self, cis: Vec<ConstantInfo>) -> Result<(), EnvError>

Add a group of constants as a unit: every one of them, or none.

The whole group is looked at before anything is inserted. When one of its names is already declared, occurs twice in the group, or belongs to a quotient constant (see Environment::add_constant), the error is returned and the environment is exactly what it was. This is how a declaration that consists of several constants — an inductive family with its constructors and recursors — is installed: a caller that added them one by one would leave the first ones behind when a later one is refused.

pub fn quot_initialized(&self) -> bool

Whether the four #QUOT primitives have been installed.

pub fn has_literal_primitives(&self) -> bool

Whether this environment declares the kernel’s own literal primitives — Nat.pred, Nat.blt, Nat.log2, String.length, String.append, String.beq — as operations without a definition, computed on literals by the reducer.

false for an empty environment, and so for every environment replayed from an export: there a constant of one of these names is whatever the file declared, and it reduces by that declaration. Lean 4’s kernel computes none of the six by name; only the operations it does compute by name (Nat.add, Nat.sub, …) are computed regardless of this flag. See reduce::lit_op_arity.

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.