Anon ingress for an entire Muts block: ingresses every member (and every constructor of every inductive member) under its deterministic projection address. Verifies that each computed address exists in `anon_env.consts` — missing → error (corrupted .ixe). Returns the KIds in member order. The first KId is the block's "primary" — `check_const` on it relies on the kernel's block coordination (`chec
( kenv: &mut KEnv<Anon>, anon_env: &IxonEnv, block_constant: &Constant, block_addr: &Address, )
| 4418 | ) -> Result<KId<Anon>, String> { |
| 4419 | let empty_meta = ConstantMeta::default(); |
| 4420 | let empty_names: FxHashMap<Address, Name> = FxHashMap::default(); |
| 4421 | let empty_n2a: FxHashMap<Name, Address> = FxHashMap::default(); |
| 4422 | let mut convert_stats = ConvertStats::new(false); |
| 4423 | let self_id: KId<Anon> = KId::new(addr.clone(), ()); |
| 4424 | |
| 4425 | let entries = match &constant.info { |
| 4426 | IxonCI::Defn(def) => ingress_defn::<Anon>( |
| 4427 | def, |
| 4428 | self_id.clone(), |
| 4429 | &empty_meta, |
| 4430 | anon_env, |
| 4431 | &empty_names, |
| 4432 | &empty_n2a, |
| 4433 | &constant.sharing, |
| 4434 | &constant.refs, |
| 4435 | &constant.univs, |
| 4436 | self_id.clone(), |
| 4437 | &mut kenv.intern, |
| 4438 | &mut convert_stats, |
| 4439 | Some(vec![self_id.clone()]), |
| 4440 | )?, |
| 4441 | IxonCI::Recr(rec) => ingress_recursor::<Anon>( |
| 4442 | rec, |
| 4443 | self_id.clone(), |
| 4444 | &empty_meta, |
| 4445 | anon_env, |
| 4446 | &empty_names, |
| 4447 | &empty_n2a, |
| 4448 | &constant.sharing, |
| 4449 | &constant.refs, |
| 4450 | &constant.univs, |
| 4451 | self_id.clone(), |
| 4452 | &mut kenv.intern, |
| 4453 | &mut convert_stats, |
| 4454 | Some(vec![self_id.clone()]), |
| 4455 | )?, |
| 4456 | _ => ingress_standalone::<Anon>( |
| 4457 | &Name::anon(), |
| 4458 | addr, |
| 4459 | constant, |
| 4460 | &empty_meta, |
| 4461 | anon_env, |
| 4462 | &empty_names, |
| 4463 | &empty_n2a, |
| 4464 | &mut kenv.intern, |
| 4465 | &mut convert_stats, |
| 4466 | )?, |
| 4467 | }; |
| 4468 | insert_standalone_entries(kenv, entries); |
| 4469 | Ok(self_id) |
| 4470 | } |
| 4471 | |
| 4472 | /// Anon ingress for a mutual inductive member. Parallel to |
| 4473 | /// `ingress_muts_inductive` but takes ctor projection addresses **directly** |
| 4474 | /// (caller computes via `anon_ctor_addrs`) and a pre-computed `mut_ctx` |
| 4475 | /// (sibling KIds for `Expr::Rec` resolution) instead of going through |
| 4476 | /// metadata. Uses `DEFAULT_ARENA` + `type_root=0` + empty level-params |
| 4477 | /// for the inductive and every ctor. |
no test coverage detected