Function resolve_all

crates/kernel/src/ingress.rs:370–388

Resolve a list of **Lean-name-hash** addresses to `KId ` pairs whose `addr` is the **projection-content address** under which the corresponding KConst is actually stored in `KEnv`. The callers (`build_mut_ctx`, `ingress_muts_inductive`'s `ctor_ids`, and `lean_all` reconstruction in `ingress_defn` / `ingress_recursor` / `ingress_muts_inductive`) pull addresses out of `ConstantMetaInfo::*::{all,

(
  all_addrs: &[Address],
  names: &FxHashMap<Address, Name>,
  name_to_addr: &FxHashMap<Name, Address>,
)

  fn synth_name(&self) -> Name {
    let n = self.synth_counter.get();
    self.synth_counter.set(n + 1);
    Name::str(Name::anon(), format!("_s{n}"))
  }
}

fn resolve_level_params(
  lvl_addrs: &[Address],
  names: &FxHashMap<Address, Name>,
) -> Vec<Name> {
  lvl_addrs.iter().map(|a| resolve_name(a, names)).collect()
}

/// Resolve a list of **Lean-name-hash** addresses to `KId<M>` pairs whose
/// `addr` is the **projection-content address** under which the corresponding
/// KConst is actually stored in `KEnv`.
///
/// The callers (`build_mut_ctx`, `ingress_muts_inductive`'s `ctor_ids`, and
/// `lean_all` reconstruction in `ingress_defn` / `ingress_recursor` /
/// `ingress_muts_inductive`) pull addresses out of `ConstantMetaInfo::*::{all,
/// ctx, ctors}`. Those fields store **name-hash** addresses (they were written
/// by compile via `compile_name`), but each KConst is stored in `KEnv` under
/// its **projection** address (the content hash of the `IPrj` / `CPrj` / `RPrj`