Method build_flat_block

crates/kernel/src/inductive.rs:491–602

Build the "flat" block for recursor generation, detecting nested occurrences. Mirrors lean4lean's `ElimNestedInductive.run`: walks constructor fields, detects `ExtInd(block_member_ref)` patterns, and adds auxiliary entries for each nested external inductive. Queue-based for transitive nesting.

(
    &mut self,
    block_inds: &[KId<M>],
    n_rec_params: u64,
    univ_offset: u64,
  )

        match w.data() {
          ExprData::All(_, _, dom, body, _) => {
            if expr_mentions_any_addr(dom, block_addrs) {
              return Ok(true);
            }
            ty = body.clone();
          },
          _ => break,
        }
      }
    }
    Ok(false)
  }

  /// Build the "flat" block for recursor generation, detecting nested occurrences.
  ///
  /// Mirrors lean4lean's `ElimNestedInductive.run`: walks constructor fields,
  /// detects `ExtInd(block_member_ref)` patterns, and adds auxiliary entries
  /// for each nested external inductive. Queue-based for transitive nesting.
  fn build_flat_block(
    &mut self,
    block_inds: &[KId<M>],
    n_rec_params: u64,
    univ_offset: u64,
  ) -> Result<Vec<FlatBlockMember<M>>, TcError<M>> {
    let anon = || M::meta_field(ix_common::env::Name::anon());
    let all_block_addrs: Vec<Address> =
      block_inds.iter().map(|id| id.addr.clone()).collect();

    let mut flat: Vec<FlatBlockMember<M>> = Vec::new();
    // (ext_ind_addr, spec_params content hashes) for dedup.
    // Uses [u8; 32] blake3 digest for structural equality.
    let mut aux_seen: Vec<(Address, Vec<KExpr<M>>)> = Vec::new();

    // Seed with original block inductives.
    for ind_id in block_inds {
      let (own_params, n_indices, ctors, lvls) = match self.get_const(ind_id)? {
        KConst::Indc { params, indices, ctors, lvls, .. } => {
          (params, indices, ctors.clone(), lvls)
        },
        _ => continue,
      };
      let ind_us = self.mk_ind_univs(lvls, univ_offset);
      let spec_params: Vec<KExpr<M>> = (0..n_rec_params)
        .map(|j| KExpr::var(n_rec_params - 1 - j, anon()))
        .collect();
      flat.push(FlatBlockMember {
        id: ind_id.clone(),
        is_aux: false,
        spec_params,
        own_params,
        n_indices,
        ctors,
        lvls,
        ind_us: ind_us.clone(),
        occurrence_us: ind_us,
      });
    }

    // Queue-based processing: scan each member's ctors for nested occurrences.