| 5042 | if gen_rules.is_empty() && !stored_rules.is_empty() { |
| 5043 | // C1: Generator produced no canonical rules but Lean stored |
| 5044 | // some — we cannot verify the stored rules against a missing |
| 5045 | // canonical form. MUST NOT accept. |
| 5046 | return Err(TcError::Other(format!( |
| 5047 | "check_recursor: rule generation failed for {}, cannot verify {} stored rules", |
| 5048 | &ind_id.addr.hex()[..8], |
| 5049 | stored_rules.len() |
| 5050 | ))); |
| 5051 | } else if !gen_rules.is_empty() && stored_rules.is_empty() { |
| 5052 | // Dual of C1: generator produced N canonical rules but Lean |
| 5053 | // stored none. Also a real mismatch. |
| 5054 | return Err(TcError::Other(format!( |
| 5055 | "check_recursor: stored recursor has no rules (expected {})", |
| 5056 | gen_rules.len() |
| 5057 | ))); |
| 5058 | } else if gen_rules.len() != stored_rules.len() { |
| 5059 | return Err(TcError::Other(format!( |
| 5060 | "check_recursor: rule count mismatch: gen={} stored={}", |
| 5061 | gen_rules.len(), |
| 5062 | stored_rules.len() |
| 5063 | ))); |
| 5064 | } |
| 5065 | // Element-wise comparison. Vacuous when both sides are empty |
| 5066 | // (zero-constructor inductives), which is the agreement case. |
| 5067 | for (ri, (gen_rule, stored_rule)) in |