Function poly_nested_rec_binder_count

crates/kernel/src/inductive.rs:5536–5561

()

        ty: cons_ty,
      },
    );

    env.blocks.insert(
      block,
      vec![mk_id("PTree"), mk_id("PTree.leaf"), mk_id("PTree.node")],
    );
    env.blocks.insert(
      mk_id("List"),
      vec![mk_id("List"), mk_id("List.nil"), mk_id("List.cons")],
    );
    env
  }

  #[test]
  fn poly_nested_flat_block() {
    let mut env = poly_nested_env();
    let mut tc = TypeChecker::new(&mut env);
    // Check inductive first (consumes fuel for validation)
    tc.check_const(&mk_id("PTree")).unwrap();
    // Reset fuel and generate recursors explicitly
    tc.rec_fuel = super::super::tc::max_rec_fuel();
    let block = mk_id("PTree");
    if !tc.env.recursor_cache.contains_key(&block) {
      tc.generate_block_recursors(&block).unwrap();
    }

    let generated =
      tc.env.recursor_cache.get(&block).expect("recursor should be cached");
    assert_eq!(