Function lean_expr_to_zexpr_cached

crates/kernel/src/ingress.rs:2250–2288

(
  expr: &LeanExpr,
  param_names: &[Name],
  binder_names: &mut Vec<Name>,
  intern: &mut InternTable<Meta>,
  n2a: Option<&DashMap<Name, Address>>,
  aux_n2a: Option<&DashMap<Name, Address>>,
  mut

  // Returns `TcError::NonCanonicalBlock` on failure, propagated as the
  // string error variant `ingress_muts_block` already returns.
  let mut indcs: Vec<(KId<M>, &KConst<M>)> = Vec::new();
  for (id, c) in &results {
    if matches!(c, KConst::Indc { .. }) {
      indcs.push((id.clone(), c));
    }
  }
  let all_primary_indc = !indcs.is_empty()
    && indcs.len()
      == members.iter().filter(|m| matches!(m, IxonMutConst::Indc(_))).count();
  if all_primary_indc
    && members.iter().all(|m| matches!(m, IxonMutConst::Indc(_)))
  {
    // Resolve a ctor by id by scanning the ingested results — simpler
    // than threading the env, since the comparator only needs Ctor
    // payloads for Indc ctors.
    let results_ref: &Vec<(KId<M>, KConst<M>)> = &results;
    let resolve_ctor = |cid: &KId<M>| -> Option<KConst<M>> {
      results_ref.iter().find(|(rid, _)| rid == cid).map(|(_, c)| c.clone())
    };
    crate::canonical_check::validate_canonical_block_single_pass::<M>(
      entry_addr,
      &indcs,
      &resolve_ctor,
    )
    .map_err(|e| format!("{e}"))?;
  }

  Ok(results)
}

// ============================================================================
// Lightweight LeanExpr → KExpr ingress (compile-side)
// ============================================================================

use ix_common::env::{
  Expr as LeanExpr, ExprData as LeanExprData, Level, LevelData,
};

/// Convert a Lean Level to KUniv<Meta>, mapping named params to positional indices.
pub fn lean_level_to_kuniv(lvl: &Level, param_names: &[Name]) -> KUniv<Meta> {
  match lvl.as_data() {
    LevelData::Succ(l, _) => KUniv::succ(lean_level_to_kuniv(l, param_names)),