Struct EnvId 

pub struct EnvId(/* private fields */);

Identity of a hash-consed LOCAL TYPING ENVIRONMENT — the fragment of a Context that decides a term’s type, and therefore half of the key an inferType cache must have.

A Term names its variables. Var("x") interns to ONE TermId whatever scope it is in, and Context::extend SHADOWS, so the same id has type Nat under one context and Bool under another. A cache keyed on the term alone would hand the second context the first’s answer — the kernel certifying a type the term does not have. That is not a hazard Lean shares: its Expr uses de Bruijn indices and globally-unique FVarIds, so two occurrences in different scopes are literally different Exprs and inferType may cache on the expression alone. Ours may not, and this is the missing half.

Implementations

impl EnvId

pub const EMPTY: EnvId

The EMPTY environment — the key every CLOSED subterm gets, and the reason the cache pays off: a closed subterm is checked once for the whole call however many scopes it occurs under.

pub fn index(self) -> usize

The dense index this handle occupies.

Trait Implementations

impl Clone for EnvId

fn clone(&self) -> EnvId

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for EnvId

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

Formats the value using the given formatter.

impl Hash for EnvId

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl Ord for EnvId

fn cmp(&self, other: &EnvId) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

impl PartialEq for EnvId

fn eq(&self, other: &EnvId) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl PartialOrd for EnvId

fn partial_cmp(&self, other: &EnvId) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

Tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

Tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl Copy for EnvId

impl Eq for EnvId

impl StructuralPartialEq for EnvId