Method contains_key

crates/kernel/src/env.rs:488–490 · view source on GitHub ↗

(&self, id: &KId<M>)

Source from the content-addressed store, hash-verified

486	/// `whnf_no_delta_for_def_eq` from scratch (mathlib hot path).
487	pub whnf_no_delta_cheap_cache: FxHashMap<(Addr, CtxAddr), KExpr<M>>,
488	/// WHNF core cache: structural-only reduction (beta/iota/zeta/proj),
489	/// no native primitives, no delta. Mirrors lean4lean's `whnfCoreCache`
490	/// (refs/lean4lean/Lean4Lean/TypeChecker.lean:19) and lean4 C++'s
491	/// `m_whnf_core`. Populated only when flags are FULL — cheap-projection
492	/// results are not safe to share with full callers.
493	pub whnf_core_cache: FxHashMap<(Addr, CtxAddr), KExpr<M>>,

contains_constMethod · 0.45

insert_addr_aliasesFunction · 0.45

ingress_const_into_kenv_with_lookups_implFunction · 0.45

ingress_addr_set_into_kenvFunction · 0.45

verify_proj_addr_in_envFunction · 0.45

ingress_anon_addr_shallowFunction · 0.45

check_inductive_memberMethod · 0.45

check_recursor_memberMethod · 0.45

poly_nested_flat_blockFunction · 0.45

poly_nested_rec_binder_countFunction · 0.45

syntax_like_flat_blockFunction · 0.45

syntax_like_false_positive_rec_fieldFunction · 0.45

no outgoing calls

poly_nested_flat_blockFunction · 0.36

poly_nested_rec_binder_countFunction · 0.36

syntax_like_flat_blockFunction · 0.36

syntax_like_false_positive_rec_fieldFunction · 0.36

syntax_like_rec_binder_countFunction · 0.36

inline_like_flat_blockFunction · 0.36

inline_like_rec_2_binder_countFunction · 0.36