Struct Env 

pub struct Env {
    pub count: usize,
    pub quot_init: bool,
    pub quotients: Vec<QuotNames>,
    /* private fields */
}

Constants indexed densely by NameId.

Fields

count: usize

quot_init: bool

quotients: Vec<QuotNames>

Every quotient installed whole, in the order its last constant arrived.

Implementations

impl Env

pub fn get(&self, n: NameId) -> Option<&Rc<Const>>

pub fn contains(&self, n: NameId) -> bool

pub fn constants(&self) -> impl Iterator<Item = &Rc<Const>>

Every admitted constant, in name-id order.

pub fn add(&mut self, c: Const)

pub fn add_provisional(&mut self, c: Const)

Adds a declaration that will be withdrawn with Env::remove once the check needing it is done.

pub fn remove(&mut self, n: NameId)

Withdraws a provisional declaration.

pub fn is_settled(&self, n: NameId) -> bool

Whether results derived from n may outlive the current declaration.

pub fn inductive(&self, n: NameId) -> Option<&InductiveInfo>

pub fn ctor(&self, n: NameId) -> Option<&CtorInfo>

pub fn rec(&self, n: NameId) -> Option<&RecInfo>

pub fn is_non_rec_structure(&self, n: NameId) -> bool

A non-recursive inductive with one constructor and no indices: the types with struct-η.

pub fn eliminates_into_every_sort(&self, n: NameId) -> bool

Whether the inductive n eliminates into every universe: its own recursor takes one universe parameter, its motive’s, beyond the inductive’s. A proposition that eliminates only into Prop takes none, and a proposition that eliminates into every universe has only proofs for fields.

Trait Implementations

impl Clone for Env

fn clone(&self) -> Env

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Default for Env

fn default() -> Env

Returns the “default value” for a type.