verus-lang / verus

Verified Rust for low-level systems code
MIT License
1.06k stars 58 forks source link

Fix missing type annotation in examples in vstd/seq.rs. #1168

Closed XuhengLi closed 1 week ago

XuhengLi commented 2 weeks ago

Some examples in vstd/seq.rs throw types errors due to missing type annotations over integer literals when initializing a Seq.

It is also worth noting that it only happens when the sequence only contains positive numbers, in which case the type checker cannot determine whether the number is an int or nat.