Function syntax_like_rec_binder_count

crates/kernel/src/inductive.rs:5900–5933

()

    assert_eq!(rules.len(), 2, "Nat.rec should have 2 rules");

    // Rule 0 (zero): fields=0
    assert_eq!(rules[0].fields, 0);
    // rhs = λ (motive) (h_zero) (h_succ), h_zero
    // = Lam(_, Lam(_, Lam(_, Var(1))))
    // Var(1) = h_zero (2nd from top: Var(0)=h_succ, Var(1)=h_zero)
    let _expected_zero = lam(
      pi(cnst("Nat", &[]), AE::sort(param(0))), // motive type (placeholder domain)
      lam(
        app(var(0), cnst("Nat.zero", &[])), // h_zero type (placeholder)
        lam(
          KExpr::sort(KUniv::zero()), // h_succ type (placeholder, won't be checked structurally)
          var(1),                     // h_zero
        ),
      ),
    );
    // Just check the BODY structure — the lambda domains don't matter for iota,
    // only the body does. Let's check fields and that the rule is well-formed.
    // For now, just verify the rule exists and has the right field count.

    // Rule 1 (succ): fields=1
    assert_eq!(rules[1].fields, 1);
    // rhs body (after applying 3 pmm + 1 field = 4 lambdas):
    // h_succ n (Nat.rec motive h_zero h_succ n)
    // Check the rhs has the right lambda count
    let count_lams = |e: &AE| -> usize {
      let mut n = 0;
      let mut c = e.clone();
      while let ExprData::Lam(_, _, _, body, _) = c.data() {
        n += 1;
        c = body.clone();
      }
      n
    };
    // pmm = 0 params + 1 motive + 2 minors = 3, plus 1 field = 4 lambdas
    let n_lams = count_lams(&rules[1].rhs);
    assert_eq!(