(
&self,
label: &str,
block_id: &KId<M>,
flat: &[FlatBlockMember<M>],
n_originals: usize,
)
| 1398 | // aux's "internal" type — what `mem.typ` becomes after |
| 1399 | // compile-side's `instantiate_pi_params(j_type_inst, |
| 1400 | // ext_n_params, &spec_params)` step. |
| 1401 | let mut typ = |
| 1402 | self.instantiate_univ_params(&ext_ty, &member.occurrence_us)?; |
| 1403 | for j in 0..ext_n_params { |
| 1404 | let w = self.whnf(&typ)?; |
| 1405 | match w.data() { |
| 1406 | ExprData::All(_, _, _, body, _) => { |
| 1407 | let body = body.clone(); |
| 1408 | let p_idx = u64_to_usize::<M>(j)?; |
| 1409 | if p_idx >= member.spec_params.len() { |
| 1410 | break; |
| 1411 | } |
| 1412 | let p = member.spec_params[p_idx].clone(); |
| 1413 | typ = subst(&mut self.env.intern, &body, &p, 0); |
| 1414 | }, |
| 1415 | _ => break, |
| 1416 | } |
| 1417 | } |
| 1418 | typ = self.replace_aux_refs_for_sort( |
| 1419 | &typ, |
| 1420 | aux, |
| 1421 | &aux_ids, |
| 1422 | block_us, |
| 1423 | n_block_params, |
| 1424 | 0, |
| 1425 | )?; |
| 1426 | // Wrap with `∀ block_params → body` to mirror compile-side |
| 1427 | // `mk_forall(j_type_block, &block_param_decls)`. The body's free Vars |
| 1428 | // for i < n_block_params already refer to the block params via the |
no test coverage detected