Get a blob by address.

Serialize: mask (Tag0) + field values in mask order.

Build a Lean String from a Rust &str.

Builds a [`RefGraph`] from a Lean [`Env`] by collecting all constant references in parallel. For each constant, extracts the set of names it referenc

Helper: `∀ (name : domain), body` with default binder info.

Walk two expressions in lockstep under `ctx` and `corr`. - `Fvar`: resolve orig's FVar through `corr`; accept if gen has the mapped FVar (or if orig'

Walk an expression and replace auxiliary const references. Memoizes on `e`'s structural hash. DAG-shared subterms are visited once regardless of how

Count the number of leading forall binders in an expression.

Decode Array Address.

Pop the most recent local variable.

Semantic universe equality: `u ≡ v` for all parameter assignments.

Add Eq.{u} and Eq.refl.{u} as axioms to the environment. Eq : {α : Sort u} → α → α → Prop Eq.refl : {α : Sort u} → (a : α) → Eq a a

Number of fvars generated so far. Used by Stage B to save/restore the counter when needed (rare; binder open/close are usually nested in a way that do

Decode Ixon.Definition. Lean stores scalar fields ordered by size (largest first). Layout: header(8) + typ(8) + value(8) + lvls(8) + kind(1) + safety(

Current logical binding depth. During the FVar transition, some code pushes legacy de-Bruijn locals into `ctx` while newer code opens binders into `l

Returns the type of this constant.

True if this level is definitionally zero (Prop).

Raw `Level::max` (no simplification) — what Lean's exporter and `Level.instantiateParams` produce.

Convert a Nat to u64, returning an error if the value is too large.

Every `env.consts` key this item certifies (proves) well-typed when its `primary` is checked — the *proven targets*, in the same address space as `Con

Substitute universe parameters in expressions.

Wrap a LeanExpr in pre-decompiled mdata layers. The `lean_mdata` vec stores layers outermost-first. We iterate in reverse to wrap innermost-first: gi

Cheap beta reduction: peephole-reduce `App(λ...λ. body, args)` shapes without invoking the full [`subst`] machinery in trivial cases. Mirrors `lean4l

Delta unfold: unfold one defined constant.

Look up a name.

Pop locals pushed by `push_locals`.

Targeted rewrite of nested type universe levels in constructor fields. Lean's kernel recomputes nested type universes from the element's sort (via `e

A distinct address for each `n` (more than the 256 `addr(u8)` affords), for fixtures large enough to exercise the multilevel coarsening path. Big-endi

Collect all constant names referenced in a LeanExpr. Uses an explicit stack to avoid stack overflow on deeply nested expressions.

Compile an entire Lean environment with explicit resource/correctness options. See [`CompileOptions`] for the intended call-site split between trusted

Generate `.below` constants for all classes in a block. For Type-level inductives: generates a `BelowDef` (reducible definition). For Prop-level indu

Deserialize an expression from bytes (iterative to avoid stack overflow).

Cached variant that takes a full `KEnv` reference instead of just `InternTable`. Uses the KEnv's `ingress_cache` to avoid re-converting shared LeanExp

Name → Address for KId construction from Lean Names.

Pop a result from the decompilation stack, returning a structured error instead of panicking if the stack is empty (malformed Ixon data).

Inverse of [`instantiate_rev`]: replace each occurrence of the listed fvars in `body` with the appropriate `Var(level)` and shift other loose bvars up

Analyze expressions for sharing opportunities within a block. Returns a map from content hash to SubtermInfo, and a map from pointer to hash. Uses a

Enumerate the anon-mode kernel work set from `env.consts`. Returns one `AnonWorkItem` per kernel-checkable group of constants. The total number of ch

Collect list elements as borrowed pointers (no refcount changes). Uses `LeanList::to_vec` which preserves the `'a` lifetime from the underlying Lean o

Check that a Lean `ConstantInfo` matches a `KConst<Anon>` structurally.

Convert a zero kernel expression to a Lean expression.

Returns the address as a lowercase hexadecimal string.

Convert a Lean Level to KUniv<Meta>, mapping named params to positional indices.

Constructs `max x y`.

Partition the blocks into `num_shards` shards via recursive bisection. Returns the shard id (in `0..num_shards`) for every block id. `epsilon` is the

Push a let-bound variable (type + value). WHNF will zeta-reduce references to this variable by substituting the value (lean4lean withExtendedLetCtx).

Restore source-side display names after a WHNF roundtrip that did not change the expression's kernel content hash. Kernel cache keys intentionally ig

Generate an arbitrary Expr using pointer-tree technique (no stack overflow)