Method populate_recursor_rules_from_block

crates/kernel/src/inductive.rs:3342–3566

Populate canonical recursor rules from the actual recursor block peers. `generate_block_recursors` is driven from the inductive block, where the recursor constants are not necessarily block members. With block-level recursor checking, the recursor block is available before comparing any sibling. Build the rule RHSs once from that block and store them back at the generated-recursors indices. This

(
    &mut self,
    ind_block_id: &KId<M>,
    rec_block_id: &KId<M>,
  )

      let fvar = self.intern(KExpr::var((n_binders - 1 - i) as u64, anon()));
      ctor_app = self.intern(KExpr::app(ctor_app, fvar));
    }
    conclusion = self.intern(KExpr::app(conclusion, ctor_app));

    // Fold: ∀ (ihs...) (fields...), conclusion (from inside out)
    // Pop IHs first (innermost)
    for i in (0..n_ihs).rev() {
      self.lctx.truncate(self.lctx.len() - 1);
      conclusion = self.intern(KExpr::all(
        anon(),
        bi_default(),
        ih_domains[i].clone(),
        conclusion,
      ));
    }
    // Pop fields
    for i in (0..n_fields).rev() {
      self.lctx.truncate(self.lctx.len() - 1);
      conclusion = self.intern(KExpr::all(
        anon(),
        bi_default(),
        field_domains[i].clone(),
        conclusion,
      ));
    }

    self.lctx.truncate(saved);
    Ok(conclusion)
  }

  /// Build an IH type for a recursive field.
  ///
  /// For a direct recursive field (type = `I_bi params idx_args`):
  ///   IH = `motive_bi(idx_args, field_var)`
  ///
  /// For a forall-wrapped recursive field (type = `∀ xs, I_bi params idx_args(xs)`):
  ///   IH = `∀ xs, motive_bi(idx_args(xs), field xs)`
  ///
  /// Called when depth = minor_saved + n_fields + k (k IHs already pushed).
  fn build_direct_ih(
    &mut self,
    field_idx: usize,
    block_ind_idx: usize,
    n_params: usize,
    n_fields: usize,
    k: usize,           // number of IHs already pushed before this one
    minor_saved: usize, // depth at entry of build_minor_at_depth
    motive_base: usize,
    field_domains: &[KExpr<M>],
    block_addrs: &[Address],
  ) -> Result<KExpr<M>, TcError<M>> {
    let anon = || M::meta_field(ix_common::env::Name::anon());
    let bi_default = || M::meta_field(ix_common::env::BinderInfo::Default);

    // Lift the field domain from its original depth (minor_saved + field_idx)
    // to the current depth (minor_saved + n_fields + k).
    let dom = &field_domains[field_idx];
    let fields_and_ihs = checked_binder_sum::<M>(
      "generated minor field + induction-hypothesis depth",