-{"file": "src/runtime/print.zig", "op": "cmp_gt_to_ge", "before": "while (ks.tag() == .list and list_collection.countOf(ks) > 0) : (ks = list_collection.rest(ks)) {", "reason": "Ranges of every callee in the predicate, which is what decides this. map_collection.keys returns Value.nil_val for an empty map (the .array_map arm via keysArrayMap's `am.count == 0` guard, the .hash_map arm via `phm.root orelse`, and the .nil arm directly), and otherwise a chain built only by list_mod.consHeap seeded from Value.nil_val; sorted_collection.keys is the same shape, seeding keysInto with Value.nil_val. consHeap sets .count = countPrepending(tail), whose whole range is {1, n+1, COUNT_UNKNOWN} - every value >= 1. list_collection.rest of such a cell returns cell.rest, which in that chain is either another consHeap cell or the nil_val seed. So for every ks this loop can hold, ks.tag() == .list implies countOf(ks) >= 1: the conjunct is never the reason the loop stops, and >= 0 cannot change the iteration count. NOT the general claim that no empty .list exists - one does (rt.empty_list, list.zig, .count = 0, which is what '() evaluates to; verified: (list? '()) is true and (count '()) is 0). The equivalence is specifically that keys never returns it. If keys is ever changed to return the empty-list singleton for an empty map, re-derive this. One entry covers both loops (.array_map/.hash_map and .sorted_map) - the line text is identical and matching is on file+op+before."}
0 commit comments