Code

No inv in iterators#1291

Code

Merged

jhjourdan merged 2 commits intomastercreusot-rs/creusot:masterfrom no_inv_in_iteratorscreusot-rs/creusot:no_inv_in_iteratorsCopy head branch name to clipboardDec 5, 2024

+6,803-14,361

Commits

Commits on Dec 5, 2024

• ITerator tests: remove inv(...) everywhere. This makes the specs simpler, the proofs simpler, and I don't think that in practice this is less expressive, because all that can be proven in produces.

  jhjourdan

  committed
  38c676c

  Copy full SHA for 38c676c

• Update stdlib accordingly.

  jhjourdan

  committed
  13fe73c

  Copy full SHA for 13fe73c