Skip to content

Commit dfcb2c0

Browse files
authored
Minor (#187)
1 parent aab3af4 commit dfcb2c0

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

vstd_extra/src/map_extra.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -256,7 +256,7 @@ pub broadcast proof fn lemma_value_filter_choose<K, V>(m: Map<K, V>, f: spec_fn(
256256
if value_filter(m, f).dom().finite() {
257257
axiom_set_choose_len(value_filter(m, f).dom());
258258
} else {
259-
axiom_set_choose_finite(value_filter(m, f).dom());
259+
axiom_set_choose_infinite(value_filter(m, f).dom());
260260
}
261261
}
262262

0 commit comments

Comments
 (0)