Method build_rule_ih

crates/kernel/src/inductive.rs:3839–3957

Build an IH value for a recursive field in a rule RHS. Direct case (field type = `I_bi params idx_args`): IH = `rec[target] params motives minors idx_args field` Forall-wrapped case (field type = `∀ (xs...), I_bi params idx_args(xs)`): IH = `λ (xs...), rec[target] params motives minors idx_args(xs) (field xs...)`

(
    &mut self,
    field_idx: u64,
    n_fields: u64,
    total_lams: u64,
    target_bi: usize,
    flat: &[FlatBlockMember<M>],
    peer_recs: &[KId<M>],
    n_rec_params: usize,
    n_motives: us

    }

    if rec_ids.len() != flat.len() {
      return Ok(None);
    }

    let mut result: Vec<KId<M>> = Vec::with_capacity(flat.len());
    for (fi, member) in flat.iter().enumerate() {
      let rec_id = &rec_ids[fi];
      let (params, motives, minors, indices, ty) =
        match self.try_get_const(rec_id)? {
          Some(KConst::Recr {
            params, motives, minors, indices, ty, ..
          }) => (params, motives, minors, indices, ty.clone()),
          _ => return Ok(None),
        };
      let skip = checked_metadata_sum::<M>(
        "recursor major index",
        &[params, motives, minors, indices],
      )?;
      let major_id = match self.get_major_inductive_id(&ty, skip) {
        Ok(id) => id,
        Err(TcError::UnknownConst(addr)) => {
          return Err(TcError::UnknownConst(addr));
        },
        Err(_) => return Ok(None),
      };
      if major_id.addr != member.id.addr {
        return Ok(None);
      }
      if !member.is_aux {
        result.push(rec_id.clone());
        continue;
      }
      // Auxiliary: verify spec_params match the stored major's param args.
      let saved = self.lctx.len();
      let mut cur = ty;
      for _ in 0..skip {
        match self.whnf(&cur) {
          Ok(w) => match w.data() {
            ExprData::All(_, _, dom, b, _) => {
              let _ = self.push_fvar_decl_anon(dom.clone());
              cur = b.clone();
            },
            _ => break,
          },
          _ => break,
        }
      }
      let mut matched = false;
      if let Ok(w) = self.whnf(&cur)
        && let ExprData::All(_, _, dom, _, _) = w.data()
      {
        let (_, major_args) = collect_app_spine(dom);
        let n_par = match u64_to_usize::<M>(member.own_params) {
          Ok(n) => n,
          Err(_) => return Ok(None),
        };
        if major_args.len() >= n_par && member.spec_params.len() == n_par {
          let n_rec_params = flat.first().map_or(0, |m| m.own_params);