Method get_major_inductive_id

crates/kernel/src/whnf.rs:1616–1663

Get the major premise's inductive KId from a recursor type. Strategy: peel `skip` foralls per Lean's stored `params + motives + minors + indices` count, then expect the next forall's domain to have an inductive `Const` head. For well-formed Lean recursors this lands exactly on the major premise. Resilience: if the strict `skip` position's domain head is not an inductive `Const`, peel up to `MAX_

(
    &mut self,
    rec_ty: &KExpr<M>,
    skip: u64,
  )

    let Some((base, offset)) = self.nat_offset(e, 0)? else {
      return Ok(None);
    };
    if offset.0 == num_bigint::BigUint::ZERO {
      return Ok(None);
    }

    let pred_offset = Nat(&offset.0 - 1u64);
    let pred = if pred_offset.0 == num_bigint::BigUint::ZERO {
      base
    } else {
      let pred_lit = self.nat_expr_from_value(pred_offset);
      self.mk_nat_add(base, pred_lit)
    };
    Ok(Some(self.mk_nat_succ(pred)))
  }

  fn nat_offset(
    &mut self,
    e: &KExpr<M>,
    depth: u16,
  ) -> Result<Option<(KExpr<M>, Nat)>, TcError<M>> {
    const MAX_NAT_OFFSET_DEPTH: u16 = 256;
    if depth >= MAX_NAT_OFFSET_DEPTH {
      return Ok(None);
    }

    let (head, args) = collect_app_spine(e);
    let ExprData::Const(id, _, _) = head.data() else {
      return Ok(None);
    };

    if id.addr == self.prims.nat_succ.addr && args.len() == 1 {
      let (base, offset) = self.nat_offset_or_zero(&args[0], depth + 1)?;
      return Ok(Some((base, Nat(offset.0 + 1u64))));
    }

    if id.addr == self.prims.nat_add.addr && args.len() == 2 {
      let Some(rhs) = self.eval_nat_offset_literal(&args[1], depth + 1) else {
        return Ok(None);
      };
      let (base, offset) = self.nat_offset_or_zero(&args[0], depth + 1)?;
      return Ok(Some((base, Nat(offset.0 + rhs.0))));
    }

    Ok(None)
  }

  fn nat_offset_or_zero(
    &mut self,
    e: &KExpr<M>,
    depth: u16,
  ) -> Result<(KExpr<M>, Nat), TcError<M>> {