Method generate_block_recursors

crates/kernel/src/inductive.rs:2213–2468

Generate recursors for all inductives in a block (lean4lean-style). Detects nested occurrences (à la `ElimNestedInductive`), builds a flat block with auxiliary entries, and generates canonical recursor types for all block members (original + auxiliary).

(
    &mut self,
    block_id: &KId<M>,
  )

        // Must be either:
        // 1. A direct block inductive application: `I_k params args`
        // 2. A nested inductive application: `J Ds is` where J is a previously
        //    declared inductive and Ds contain block inductives
        let (head, args) = collect_app_spine(&w);
        match head.data() {
          ExprData::Const(id, us, _) if root_addrs.contains(&id.addr) => self
            .check_positive_recursive_application(
              id, us, &args, groups, root_addrs,
            ),
          ExprData::Const(id, us, _) => {
            // Check if this is a nested inductive: head is an inductive type
            // (not in our block) and its params contain block inductives.
            let (n_params, n_indices, lvls, block, ctors) = match self
              .get_const(id)?
            {
              KConst::Indc { params, indices, lvls, block, ctors, .. } => (
                u64_to_usize(params)?,
                u64_to_usize(indices)?,
                u64_to_usize(lvls)?,
                block.clone(),
                ctors.clone(),
              ),
              _ => {
                return Err(TcError::Other(
                  "positivity: not a valid inductive app".into(),
                ));
              },
            };

            let app_arity = checked_binder_sum::<M>(
              "positivity nested application",
              n_params,
              n_indices,
            )?;
            if args.len() != app_arity || us.len() != lvls {
              return Err(TcError::Other(
                "positivity: malformed nested inductive application".into(),
              ));
            }

            // An exact repeated specialization is the recursive edge of an
            // already-validated synthetic auxiliary. A different
            // specialization of the same external family is a distinct
            // auxiliary (for example both `Array (ListItem (Block i b))`
            // and `Array (Block i b)` in `Lean.Doc.Block`).
            let existing_groups: Vec<PositivityGroup<M>> = groups
              .iter()
              .filter(|group| group.addrs.contains(&id.addr))
              .cloned()
              .collect();
            for group in &existing_groups {
              if Self::positivity_group_matches(
                group, &id.addr, us, &args, n_params,
              ) {
                for index in args.iter().skip(n_params) {
                  if expr_mentions_any_addr(index, root_addrs) {
                    return Err(TcError::Other(
                      "positivity: recursive occurrence index mentions an active inductive"
                        .into(),