Method synth_ctor_when_k

crates/kernel/src/whnf.rs:1319–1384

For K-like recursors, try to synthesize a nullary constructor from the major premise's type. Returns `Ok(Some(ctor_app))` if successful. Algorithm (following lean4lean/nanoda): 1. Infer major's type, WHNF it 2. Check head constant matches the recursor's target inductive 3. Build nullary ctor: `Ctor.{levels} params...` 4. Infer ctor's type, check def-eq with major's type

(
    &mut self,
    major: &KExpr<M>,
    rec_id: &KId<M>,
    recr: &IotaInfo<M>,
  )

        k,
        params,
        motives,
        minors,
        indices,
        rules,
        lvls,
        ..
      }) => {
        let major_idx = u64_to_usize::<M>(params + motives + minors + indices)?;
        if spine.len() <= major_idx {
          return Ok(None);
        }
        IotaInfo {
          k,
          params: u64_to_usize::<M>(params)?,
          motives: u64_to_usize::<M>(motives)?,
          minors: u64_to_usize::<M>(minors)?,
          indices: u64_to_usize::<M>(indices)?,
          major_idx,
          // `rules` is already owned here (moved out of the KConst clone
          // `try_get_const` returned) — do not clone it again.
          rules,
          lvls,
        }
      },
      _ => return Ok(None),
    };

    // K-like recursor: try to synthesize a nullary constructor before WHNF.
    // This handles cases like `Eq.rec motive minor major` where major isn't
    // a constructor but its type matches the inductive — we build `Eq.refl params...`.
    let major = &spine[recr.major_idx];
    let major = if recr.k {
      self
        .synth_ctor_when_k(major, &rec_id, &recr, &rec_us)?
        .unwrap_or_else(|| major.clone())
    } else {
      major.clone()
    };
    let major = match self.cleanup_nat_offset_major(&major)? {
      Some(cleaned) => cleaned,
      None => major,
    };

    // WHNF the major premise. Cheap mode skips delta on the major itself,
    // matching Lean4Lean's `cheapRec` (TypeChecker.lean:337–341); the rest of
    // the iota machinery still gets a structural normal form to inspect.
    let mut major_whnf = if flags.cheap_rec {
      self.whnf_core_with_flags(&major, flags)?
    } else {
      self.whnf(&major)?
    };

    // Nat literal → constructor form (one level: n → Nat.succ(lit(n-1))).
    //
    // Mirrors lean4 (`refs/lean4/src/kernel/inductive.h:91-93`) and
    // lean4lean (`refs/lean4lean/Lean4Lean/Inductive/Reduce.lean:70`):
    // unconditional peel. Truly runaway recursors (step case forces the
    // IH on every iteration) are bounded by `MAX_WHNF_FUEL` / outer