Method compute_k_target

crates/kernel/src/inductive.rs:4456–4494

S1: Compute K-target flag constructively. K-like reduction is sound iff: 1. Single inductive (not part of a mutual block with >1 inductive) 2. Result universe is Prop (level is zero) 3. Exactly one constructor with zero non-param fields

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

          };
          field_domains.push(lifted_dom);
          minor_cur = b.clone();
        },
        _ => break,
      }
    }
    // Wrap in reverse: last field innermost, first field outermost.
    // This ensures Var(n_fields-1) = first field, Var(0) = last field,
    // matching the body's de Bruijn indexing.
    for i in (0..field_domains.len()).rev() {
      body = self.intern(KExpr::lam(
        anon(),
        bi_default(),
        field_domains[i].clone(),
        body,
      ));
    }

    // PMM lambdas: extract actual domains from the peer recursor's type.
    // The recursor type has the shape:
    //   ∀ (params...) (motives...) (minors...) (indices...) (major), ret
    // We need the first pmm domains for the rule's leading lambdas.
    // Do NOT instantiate universe params: the rule RHS and recursor type share
    // the same Param references. The stored rule was built by Lean with the same
    // Param indices as the recursor type.
    let mut pmm_domains: Vec<KExpr<M>> = Vec::with_capacity(pmm);
    let mut rec_ty_cur = rec_ty_for_member.clone();
    for _ in 0..pmm {
      let w = self.whnf(&rec_ty_cur)?;
      match w.data() {
        ExprData::All(_, _, dom, b, _) => {
          pmm_domains.push(dom.clone());
          rec_ty_cur = b.clone();
        },
        _ => {
          // Fallback to placeholder if recursor type is shorter than expected
          pmm_domains.push(KExpr::sort(KUniv::zero()));
          break;
        },
      }
    }
    // Wrap body in PMM lambdas (inside-out: minors, then motives, then params)
    // pmm_domains is [p0, ..., pk, m0, ..., ml, min0, ..., minr]