Method len

crates/kernel/src/env.rs:480–482 · view source on GitHub ↗

(&self)

Source from the content-addressed store, hash-verified

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

find_duplicatesFunction · 0.45

prim_addrs_new_no_unexpected_duplicatesFunction · 0.45

validate_expr_well_scopedMethod · 0.45

check_eq_typeMethod · 0.45

count_forallsMethod · 0.45

meta_fmtMethod · 0.45

fmtMethod · 0.45

simul_subst_cachedFunction · 0.45

cheap_beta_reduceFunction · 0.45

instantiate_rev_cachedFunction · 0.45

abstract_fvarsFunction · 0.45

quick_def_eqMethod · 0.45

no outgoing calls

prim_addrs_new_no_unexpected_duplicatesFunction · 0.36

def_eq_closed_cache_ignores_context_across_checkersFunction · 0.36

def_eq_open_cache_uses_relevant_context_suffixFunction · 0.36

inline_like_rec_2_binder_countFunction · 0.36

infer_closed_cache_ignores_contextFunction · 0.36

infer_open_cache_is_context_sensitiveFunction · 0.36

meta_hash_binder_info_distinctFunction · 0.36