Walk past the first `n` Pi binders of the block's first inductive type and return their `(name, BinderInfo, domain)` triples in declaration order (outermost-first). Each domain is in the recursor-external context: `domain_i` may have free `Var(j)` for `j < i` referring to block param `i-1-j` (the standard de Bruijn telescope shape, identical to how the original ind_ty stores its param binders).
(
&mut self,
block_first_id: &KId<M>,
n_block_params: u64,
)
| 947 | |
| 948 | // Retain the concrete universe spine before deduplication. It is part |
| 949 | // of Lean's nested application identity independently of the term |
| 950 | // parameter spine. |
| 951 | let occurrence_us: Box<[KUniv<M>]> = match head.data() { |
| 952 | ExprData::Const(_, us, _) => us.clone(), |
| 953 | _ => Box::new([]), |
| 954 | }; |
| 955 | |
| 956 | // Dedup the exact (external family, universes, parameters) |
| 957 | // specialization. Structural comparison uses the uid fast path plus |
| 958 | // recursive fallback, so separately-built equal inputs still collapse. |
| 959 | let spec_hashes: Vec<KExpr<M>> = spec_params.clone(); |
| 960 | if aux_seen.iter().any(|(a, seen_us, s)| { |
| 961 | same_nested_specialization( |
| 962 | a, |
| 963 | seen_us, |
| 964 | s, |
| 965 | &head_id.addr, |
| 966 | &occurrence_us, |
| 967 | &spec_hashes, |
| 968 | ) |
| 969 | }) { |
| 970 | return Ok(()); |
| 971 | } |
| 972 | aux_seen.push((head_id.addr.clone(), occurrence_us.clone(), spec_hashes)); |
| 973 | |
| 974 | // Abstract shifted universe params for internal processing (dedup, ctor walking). |
| 975 | let aux_us = self.mk_ind_univs(ext_lvls, univ_offset)?; |
| 976 | |
| 977 | flat.push(FlatBlockMember { |
| 978 | id: head_id, |
| 979 | is_aux: true, |
| 980 | spec_params, |
| 981 | own_params: ext_params, |
no test coverage detected