| 3283 | let ExprData::Const(id, _, _) = head.data() else { |
| 3284 | return None; |
| 3285 | }; |
| 3286 | if id.addr == self.prims.bit_vec_of_nat.addr && args.len() == 2 { |
| 3287 | return Some((args[0].clone(), args[1].clone())); |
| 3288 | } |
| 3289 | if id.addr != self.prims.of_nat_of_nat.addr || args.len() < 2 { |
| 3290 | return None; |
| 3291 | } |
| 3292 | |
| 3293 | let (type_head, type_args) = collect_app_spine(&args[0]); |
| 3294 | let ExprData::Const(type_id, _, _) = type_head.data() else { |
| 3295 | return None; |
| 3296 | }; |
| 3297 | if type_id.addr == self.prims.bit_vec.addr && type_args.len() == 1 { |
| 3298 | Some((type_args[0].clone(), args[1].clone())) |
| 3299 | } else { |