Push a declaration. The caller is responsible for ensuring `id` is fresh (typically from [`NameGenerator::fresh`]).

Whether the orig-side FVar `name` has a gen-side counterpart.

Returns the raw 32-byte digest.

Returns a reference to the inner [`NameData`].

Iterate over all constants. Returns owned (KId, KConst) pairs.

Intern an expression through the mutable intern environment.

Returns the precomputed Blake3 hash of this name.

Full WHNF: loop of whnf_no_delta → delta (one step).

Helper: build `App(f, a)`

Helper: build `∀ (_ : a), b`

Helper: build `Const(name, univs)`

Returns `true` if this mutual constant contains the given name (including constructor names for inductives).

Returns a dot-separated human-readable representation of this name.

Apply an expression to a sequence of arguments: `f a1 a2 ... an`.

View the bytes as a `&[u8]`. Zero-copy for both variants: `Heap` derefs the `Arc<[u8]>`; `Mmap` slices the mapping.

Collect the application spine: `App(App(f, a1), a2)` → `(f, [a1, a2])`. Counts args first so the result `Vec` is allocated exactly once with the corr

Open N leading foralls of `expr`, replacing each BVar(0) with a fresh FVar. Returns the FVars, their declarations, and the remaining body. This is th

RawEnvironment is a single-field struct, unboxed to just Array by Lean.

Append the trailing `# total failures: N` summary. Called once after all per-constant checks have reported.

Create a fresh FVar with a unique name derived from `prefix` and `idx`.

Truncate the context to the given length, dropping any declarations pushed since. The dropped fvars become unresolvable via [`Self::find`].

Type-check a single constant. Clears per-constant caches first.

Build a Nat env with Nat, Nat.zero, Nat.succ, Nat.rec, and Nat.sub. Nat.sub is defined as a primitive that the kernel's try_reduce_nat handles, but al

Build the canonical merkle root over a leaf set. Leaves are lex-sorted and deduplicated before hashing. Returns: - `None` if `leaves` is empty (post-

Check definitional equality of two expressions.

Deserialize a `System<AiurCircuit>` from [`to_bytes`] output, requiring that every byte is consumed.

Push a local variable type (lambda/forall binding, no let-value).

Create a `Const` expression with the given name and universe levels.

Compile a Lean Name to an address (stored in env.names). Uses the Name's internal hash as the address. String components are stored in blobs.

Intern an expression: same pointer-uniqueness guarantee as `intern_univ`.

Lean's `instantiate1`: replace BVar(0) with `replacement`, decrement BVar(i>0) by 1 (removing a binder level). The replacement is NOT shifted — it's i

Convert a Lean `Nat` to `usize`, panicking on overflow. Use in pure functions where returning `Result` would cascade through callers. Overflow is imp

Decompose an application spine: `f a1 a2 ... an` -> `(f, [a1, ..., an])`.

Get a constant by address, materializing on demand. Returns `None` if the address is not present or materialization fails (e.g., corrupt bytes). Use