Struct Environment 

pub struct Environment { /* private fields */ }

The global environment containing all checked declarations.

Implementations

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.

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) -> Environment

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() -> Environment

Returns the “default value” for a type.