| 173 | /// Take a borrowed Array of (Name × Level) pairs, decode all, return count. |
| 174 | #[unsafe(no_mangle)] |
| 175 | pub extern "C" fn rs_refcount_nested_borrow( |
| 176 | arr: LeanArray<LeanBorrowed<'_>>, |
| 177 | ) -> LeanOwned { |
| 178 | let mut count: u64 = 0; |
| 179 | for elem in arr.iter() { |
| 180 | let pair = elem.as_ctor(); |
| 181 | let _name = LeanIxName(pair.get(0)).decode(); |
| 182 | let _level = LeanIxLevel(pair.get(1)).decode(); |
| 183 | count += 1; |
| 184 | } |
| 185 | LeanNat::from_nat(&Nat::from(count)).into() |
| 186 | } |
| 187 | |
| 188 | // ============================================================================= |
| 189 | // Cache deduplication: build same subterm multiple times |