Function nat_rec_rules

crates/kernel/src/inductive.rs:4873–4928

()

        lvls: 1,
        params: 0,
        indices: 0,
        motives: 1,
        minors: 2,
        block: rec_block.clone(),
        member_idx: 0,
        ty: rec_ty,
        rules: vec![
          super::super::constant::RecRule {
            ctor: (),
            fields: 0,
            rhs: rule_zero_rhs,
          },
          super::super::constant::RecRule {
            ctor: (),
            fields: 1,
            rhs: rule_succ_rhs,
          },
        ],
        lean_all: (),
      },
    );

    env
      .blocks
      .insert(block, vec![mk_id("Nat"), mk_id("Nat.zero"), mk_id("Nat.succ")]);
    env.blocks.insert(rec_block, vec![mk_id("Nat.rec")]);
    env
  }

  #[test]
  fn check_nat_rec() {
    let mut env = nat_env();
    let mut tc = TypeChecker::new(&mut env);
    tc.check_const(&mk_id("Nat")).unwrap();
    assert!(tc.check_const(&mk_id("Nat.rec")).is_ok(), "Nat.rec should pass");
  }

  #[test]
  fn nat_rec_rules() {
    // Nat.rec has 2 rules (one per ctor):
    // Rule 0 (Nat.zero): fields=0, rhs = λ (motive) (h_zero) (h_succ), h_zero
    // Rule 1 (Nat.succ): fields=1, rhs = λ (motive) (h_zero) (h_succ) (n),
    //   h_succ n (Nat.rec.{Param(0), ...} motive h_zero h_succ n)
    let mut env = nat_env();
    let mut tc = TypeChecker::new(&mut env);
    tc.check_const(&mk_id("Nat")).unwrap();
    tc.check_const(&mk_id("Nat.rec")).unwrap();

    let block = mk_id("Nat");
    let generated = tc.env.recursor_cache.get(&block).unwrap();
    let rules = &generated[0].rules;

    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))))