Struct Environment 

pub struct Environment { /* private fields */ }

Global environment

Implementations

impl Environment

pub fn new() -> Self

Create a new empty environment

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

Add a declaration to the environment

pub fn get_decl(&self, name: SymbolId) -> Option<&Declaration>

Get a declaration by name

pub fn has_decl(&self, name: SymbolId) -> bool

Check if a declaration exists

pub fn add_inductive(&mut self, ind: InductiveDecl) -> Result<()>

Add an inductive type

pub fn get_inductive(&self, name: SymbolId) -> Option<&InductiveDecl>

Get an inductive type by name

pub fn get_inductive_of_constructor( &self, ctor: SymbolId, ) -> Option<&InductiveDecl>

Get the inductive type for a constructor

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

Check if a name is a constructor

pub fn declarations(&self) -> impl Iterator<Item = (&SymbolId, &Declaration)>

Get all declarations

pub fn num_decls(&self) -> usize

Get the number of declarations

pub fn fork(&self) -> Self

Clone the environment (cheap due to persistent data structures)

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 Default for Environment

fn default() -> Self

Returns the “default value” for a type.