()
| 7003 | n |
| 7004 | }; |
| 7005 | |
| 7006 | // Total top-level binders: 3 motives + 6 minors + 0 indices + 1 major = 10 |
| 7007 | let n = count_binders(&generated[0].ty); |
| 7008 | assert_eq!(n, 10, "Syn.rec with ident should have 10 binders, got {n}"); |
| 7009 | |
| 7010 | // Check the ident minor (binder 5 = 3 motives + 2 earlier minors) |
| 7011 | // Its domain should have 1 inner binder (the List Other field) and 0 IHs. |
| 7012 | // If is_rec_field falsely matches List Other, it would have 2 inner binders. |
| 7013 | let mut cur = generated[0].ty.clone(); |
| 7014 | for _ in 0..5 { |
| 7015 | // skip to binder 5 |
| 7016 | if let ExprData::All(_, _, _, body, _) = cur.data() { |
| 7017 | cur = body.clone(); |
| 7018 | } |
| 7019 | } |
| 7020 | let ident_minor_domain = match cur.data() { |
| 7021 | ExprData::All(_, _, dom, _, _) => dom.clone(), |
| 7022 | _ => panic!("expected forall at binder 5"), |
| 7023 | }; |
| 7024 | let ident_inner_binders = count_binders(&ident_minor_domain); |
| 7025 | // Should be 1 (just the List Other field), NOT 2 (field + false IH) |
| 7026 | assert_eq!( |
| 7027 | ident_inner_binders, 1, |
| 7028 | "ident minor should have 1 inner binder (non-rec field), got {} (false positive IH?)", |
| 7029 | ident_inner_binders |
| 7030 | ); |
| 7031 | } |
| 7032 | |
| 7033 | #[test] |
| 7034 | fn syntax_like_rec_binder_count() { |
nothing calls this directly
no test coverage detected