Function inline_like_rec_2_binder_count

crates/kernel/src/inductive.rs:6202–6277

()

      3,
      "flat block should have 3 members, got {}",
      generated.len()
    );
  }

  #[test]
  fn inline_like_rec_2_binder_count() {
    let mut env = inline_like_env();
    let mut tc = TypeChecker::new(&mut env);
    tc.check_const(&mk_id("Inl")).unwrap();
    tc.rec_fuel = super::super::tc::max_rec_fuel();
    let block = mk_id("Inl");
    if !tc.env.recursor_cache.contains_key(&block) {
      tc.generate_block_recursors(&block).unwrap();
    }
    let generated = tc.env.recursor_cache.get(&block).unwrap();

    let count_binders = |e: &AE| -> usize {
      let mut n = 0;
      let mut c = e.clone();
      while let ExprData::All(_, _, _, b, _) = c.data() {
        n += 1;
        c = b.clone();
      }
      n
    };

    // Inl.rec (member 0):
    //   1 param(α) + 3 motives + N minors + 0 indices + 1 major
    //   Minors: text(1f+0ih), emph(1f+1ih), other(2f+1ih), arr.mk(1f+1ih), nil(0), cons(2f+2ih)
    //   = 6 minors
    //   Total = 1 + 3 + 6 + 0 + 1 = 11
    let n0 = count_binders(&generated[0].ty);
    assert_eq!(n0, 11, "Inl.rec should have 11 binders, got {n0}");

    // Inl.rec_2 (member 2 = List aux):
    //   1 param + 3 motives + 6 minors + 0 indices + 1 major = 11
    if generated.len() > 2 {
      let n2 = count_binders(&generated[2].ty);
      assert_eq!(
        n2, 11,
        "Inl.rec_2 (List aux) should have 11 binders, got {n2}"
      );
    }

    // Deeper check: verify the generated Inl.rec_2 type against a manually
    // constructed version to catch var-index bugs.
    // For this we need the Inl.rec_2 stored as a Recr constant and compare.
    // Instead, let's just check that is_def_eq succeeds between rec[0] and
    // a hand-constructed Inl.rec.
    // This is complex, so let's at least verify that the cons minor inside
    // rec_2 has the right structure by inspecting its inner binders.

    // rec_2 = generated[2], binder layout:
    // 0: param (i : Sort(u+1))
    // 1: motive_0 (Inl motive)
    // 2: motive_1 (Array aux motive)
    // 3: motive_2 (List aux motive)
    // 4-9: minors (text, emph, other, arr.mk, nil, cons)