()
| 6659 | let mut tc = TypeChecker::new(&mut env); |
| 6660 | // Check inductive first (consumes fuel for validation) |
| 6661 | tc.check_const(&mk_id("PTree")).unwrap(); |
| 6662 | // Reset fuel and generate recursors explicitly |
| 6663 | tc.rec_fuel = super::super::tc::max_rec_fuel(); |
| 6664 | let block = mk_id("PTree"); |
| 6665 | if !tc.env.recursor_cache.contains_key(&block) { |
| 6666 | tc.generate_block_recursors(&block).unwrap(); |
| 6667 | } |
| 6668 | |
| 6669 | let generated = |
| 6670 | tc.env.recursor_cache.get(&block).expect("recursor should be cached"); |
| 6671 | assert_eq!( |
nothing calls this directly
no test coverage detected