Method recursor_dump_matches_block

crates/kernel/src/inductive.rs:1389–1398

(
    &self,
    block_id: &KId<M>,
    flat: &[FlatBlockMember<M>],
  )

          },
          _ => {
            return Err(TcError::Other(
              "canonical_aux_order: aux ext is not an inductive".into(),
            ));
          },
        };

      // Instantiate ext_ty: replace J's universe params with the
      // occurrence's universe args, then walk past `ext_n_params` Pi
      // binders, substituting with `spec_params`. The result is the
      // aux's "internal" type — what `mem.typ` becomes after
      // compile-side's `instantiate_pi_params(j_type_inst,
      // ext_n_params, &spec_params)` step.
      let mut typ =