Compute strongly connected components using an iterative Tarjan’s algorithm. Returns a map from each node to the set of nodes in its SCC.

Check that two `ConstantInfo` values are alpha-equivalent.

Strip type annotation wrappers from a type expression. Matches Lean's `Expr.consumeTypeAnnotations` (Expr.lean:1721-1727): - `outParam α` → recurse o

Convert a zero kernel constant to a Lean `ConstantInfo`.

Build a minimal env with a single definition: `id := λ x. x : Sort 0 → Sort 0`

Freeze into an immutable [`BlockProfile`]. Block ids are assigned by sorting addresses, so the result is deterministic regardless of insertion order.

Check that a Lean-side Level matches a zero Univ structurally.

Produce a sibling-path for `target` in the canonical tree over `leaves`. Returns `None` if `target` is not in the (post-dedup) leaf set. Returns an em

Total canonical-layout motive count: `n_primary + n_canonical_aux`.

Convert a LeanExpr to KExpr<Meta>. `param_names` provides the positional mapping for universe level params. `name_to_ixon_addr` maps Lean names to re

The address to pass to `tc.check_const`.

Push a fresh fvar declaration without any body to instantiate. Useful for paths that introduce a binder for type-tracking purposes only (e.g. inductiv

Constructs a sort expression from a universe level.

Nat primitive reduction (add, sub, mul, div, mod, pow, gcd, bitwise, predicates).

Structural WHNF: beta, iota, zeta. NO delta. FULL flags. This is the standard structural normalizer used outside the def-eq lazy-delta path. With `Wh

Weak-head-normalize a `LeanExpr` in the current FVar context, using our Rust kernel's `whnf`. Matches Lean's `Meta.whnf` behavior: unfolds reducible d

Def-eq no-delta WHNF. This is broader than Lean's pure `whnfCore` because Ix relies on the no-delta layer for primitive/native reductions, but it pres

Decode Ixon.RawConst from Lean pointer.

Decompile an Ixon Expr to a Lean Expr with arena-based metadata restoration. Traverses the arena tree following child pointers. Share references are

Extract a Nat value from either literal form or a constructor numeral. Iota reduction on `Nat` literals can expose the matched value as `Nat.succ <li

This replaces the BVar-range-based `is_motive_application` and `find_motive_class` with a simple structural FVar comparison.

Generate a bounded-depth `KUniv<Anon>`. Parameter indices are drawn from `0..=max_param` so multiple universes in the same test can share parameters —

Generate recursors for all inductives in a block (lean4lean-style). Detects nested occurrences (à la `ElimNestedInductive`), builds a flat block with

Count the outermost Succ wrappers. Matches Lean's `Level.getOffset`.

Get the last string component of this name, if any.

Borrow this sub-hypergraph as a [`Level`] for the greedy / FM machinery.

Absorbs the elements of the smaller [`NameSet`] into the bigger one and returns the merged set.

Serialize a universe to bytes (iterative to avoid stack overflow).

Read a Tag0-encoded u64 from a byte slice, advancing the cursor.

Store a string as a blob and return its address.

Strip a prefix from this name, returning the suffix components.

Record that two composite keys are definitionally equal. Kept by-value because `node_for_key` inserts the key into the internal `key_to_node` map on

Reduce all beta-redexes in an expression. `App(Lam(_, _, body, _), arg)` → `instantiate1(body, arg)` (then recurse). Lean's elaborator auto-reduces

Build a Lean `Array G` from a slice of field elements.

Build a Lean `Array (G × Array G) × Array ((G × Array G) × IOKeyInfo)` from an `IOBuffer`. The first array enumerates per-channel data arenas; the sec

Compare two kernel expressions structurally for canonical ordering. Alpha-blind through binders (`Lam`, `All`, `Let` ignore names) and uses `ctx` to r

Decode Ixon.DataValue.

Ensure PUnit and PProd are in `stt.kenv` for kernel type inference. These are prelude constants with fixed definitions that brecOn's `get_level` need

Check that two Lean expressions are alpha-equivalent (ignoring binder names, BinderInfo, and Mdata wrappers).

Generate a `.casesOn` definition from a canonical `.rec`. Returns `None` if the recursor type cannot be decomposed. Uses FVar-based construction: op

Generate a `.recOn` definition from a canonical `.rec`. Returns `None` if the recursor type cannot be decomposed.

Extract head constant's display form as a string, for diagnostic prefix matching. Uses `{kid}`'s Display impl (which is defined for every `KernelMode`

Convert a kernel expression to an Ixon expression, accumulating any referenced addresses and universes into `ctx`. Memoized on `expr.addr()` (content

Build the 3-slice leaf-guest stdin: range + env bytes + reuse check-list. `check_list` is a packed list of primary addresses (`Address::pack`) to che

Static version of `to_kexpr` that takes borrowed references. Identical to the closure-based `to_kexpr` in `get_level`, but as a standalone function s

Count how many bytes needed to represent a u64.

Internal flags-threaded core: callers go through [`whnf_core`] or [`whnf_core_for_def_eq`]. Recursive sub-reductions and `try_iota` propagate the same

Append suffix components to this name.

Build an env with Bool (2 ctors, 0 fields each) and its recursor. Bool : Sort 1 Bool.true : Bool Bool.false : Bool Bool.rec : ∀ (motive : Bool → Sort

Build a minimal Prop mutual block: A | a : B → A, B | b : A → B. Both A and B are in Prop (Sort 0), with single constructors that cross-reference the

Build a test env where each recursor reports `num_motives` and `num_minors` with `aux_motives` / `aux_minors` added on top of the user-visible counts.

Compile a Lean Level to an Ixon Univ.

Decide which subterms to share based on profitability. Sharing is profitable when: `(N - 1) * term_size > N * share_ref_size` where N is usage count,

Check whether an expression mentions any constant from a set of addresses.

Extract a nat value from a literal or `Nat.zero` constructor. Matches both `Nat(n)` literals and the `Nat.zero` constructor constant, mirroring C++ `