Function insert_addr_aliases

crates/kernel/src/ingress.rs:3194–3215

(
  kenv: &mut KEnv<M>,
  lookups: &IxonIngressLookups,
  addr: &Address,
)

  // mismatch` on every mutual-block recursor (we saw this on
  // `Lean.Xml.Content.rec`, `Lean.Compiler.LCNF.Code.rec`, every
  // `Grind.Arith.*.*Cnstr*.rec`, etc.).
  //
  // Declaration order is *not* the canonical structural order that
  // `sort_consts` produces during compilation — that second order
  // only shows up in the compiled `kctx.kenv`, not here. Iterating
  // `lean_env` directly to push each constant's `self_kid` gave
  // random (FxHashMap iteration) order; we now seed each block with
  // its `all` list the first time any member is observed, then
  // append ctors and recursors in a second pass. Ctors/recursors
  // land at the tail — the block's inductive-prefix carries the
  // declaration order that `discover_block_inductives` consumes.
  //
  // `ixon_ingress` builds an analogous list for `kctx.kenv`, but
  // there the ordering comes from `sort_consts`' equivalence-class
  // output (structural, not declarational). The two paths diverge on
  // purpose: `orig_kenv` carries Lean's source-order recursor
  // expectations, `kctx.kenv` carries the canonical-compile recursor
  // expectations.
  //
  // For singleton inductives, the block is keyed at `self_kid`; for
  // multi-member mutuals, at the representative (first name in `all`).
  let block_rep = |name: &Name, ci: &LeanCI| -> KId<Meta> {
    let all = lean_constant_all(ci);
    let rep =
      all.and_then(|a| a.first()).cloned().unwrap_or_else(|| name.clone());