verus
forked from verus-lang/verus
Star 0
Fork 0
Watch

Version history of source/vstd/seq_lib.rs

October 2026

Bryan Parno
Swap from will_return_none to produces (#3330)
committed
Bryan Parno
vstd: Add a broadcast to connect s.as_ref() indices to s. (#3018)
committed

September 2026

Chris Hawblitzel (Microsoft)
Apply verusfmt to vstd seq-range expressions (#3006)
committed
Chris Hawblitzel (Microsoft)
Use Seq range syntax in vstd, examples, docs (#2959)
committed
Bryan Parno
Add specs for Iterator::zip (#2858)
committed
Bryan Parno
Add specs for Iterator::filter (#2515)
committed

July 2026

Baltasar Dinis
vstd: remove usage of group_seq_axioms and added axioms (#2678)
committed

June 2026

Jay Lorch
Make `Set` and `Map` finite, add `ISet` and `IMap`. (#2486)
committed

May 2026

Bryan Parno
New approach to specifying iterators via a prophetic sequence encoding (#2163)
committed

March 2026

Chris Hawblitzel
Merge branch 'main' into make_spec_type
committed

February 2026

Chris Hawblitzel
Merge branch 'main' into assoc-const1
committed
elanortang
remove deprecated fns or update attribute (#2120)
committed

December 2025

Chris Hawblitzel
Merge branch 'main' into assoc-const1
committed

November 2025

Baltasar Dinis
docs: add CI to make sure that docs build without warnings (#2003)
committed

August 2025

ddt
vstd : add lemmas about Seq::fold_left/fold_right (#1833)
committed

July 2025

Bryan Parno
Prepare Verus-related crates for posting to crates.io (#1815)
committed
Alex Bai
Remove oudated comments in seq_lib (#1836)
committed
Chris Hawblitzel
Simplify Vec::swap_remove
committed
lyj
Vec::swap_remove (#1755)
committed

June 2025

Natalie Neamtu
Merge branch 'main' into zero-to-nat/docs-retreat-2025
committed
Alex Bai
add multiset lemmas (#1773)
committed
Chris Hawblitzel
Merge branch 'main' into loop-infer-base
committed
Marianna Rapoport
Add functions and lemmas to seq_lib (#1702)
committed
Nickolai Zeldovich
add `Seq::update_range()` to update subrange of a sequence
committed
Daniel Schoepe
Add additional `Set` functions and lemmas (#1701)
committed

May 2025

Nickolai Zeldovich
prove how Seq::fold_left distributes over subrange (#1654)
committed
nobody
Rename examples directory (rename source/rust_verify/example to examples)
committed
Alex Bai
update syntax for broadcast use (#1571)
committed

April 2025

ddt
fix vstd::seq_lib::lemma_seq_contains_after_push (#1553)
committed

February 2025

Alex Bai
fix trigger in `to_multiset_len` and `commutative_foldr` proof (#1454)
committed
Alex Bai
use broadcast for map/set/multiset_properties (#1443)
committed
Alex Bai
Seq_lib broadcasting (#1436)
committed

November 2024

Nickolai Zeldovich
Add some multiset-related lemmas (#1329)
committed

October 2024

Jon Howell
verusfmt
committed
Jon Howell
add subrange_of_matching_take lemma to seq_lib
committed

August 2024

Chris Hawblitzel (Microsoft)
Prune broadcast functions based on their triggers (#1175)
committed

July 2024

Pratap Singh
remove extraneous sentence in map_values docs (#1230)
committed

May 2024

Travis Hance
Support embedding 'builtin' and 'vstd' as modules in order to support verifying core (#1085)
committed
Chris Hawblitzel
Update verifier(...) to verifier::... in guide/examples/vstd
committed

April 2024

Andrea Lattuada
Use generalized broadcast in arithmetic library, rename all broadcast groups to have the prefix group_ (#1086)
committed
Andrea Lattuada
Merge pull request #1023 from verus-lang/generalized-broadcast-vstd
committed
Andrea Lattuada
support cfg(not(feature = "alloc")) with default vstd broadcast group, guard verifier attributes with cfg_attr where necessary
committed
Andrea Lattuada
fix failing proofs, use new broadcast mechanism for array_as_slice
committed
Andrea Lattuada
un-admit TODOS, broadcast group vstd_axioms -> vstd_default
committed
Andrea Lattuada
verusfmt
committed
Andrea Lattuada
apply generalized broadcast to vstd
committed
Jay Bosamiya
Broadcast-use formatting style change (#1062)
committed
Jay Bosamiya
Minor reformat with latest verusfmt
committed

March 2024

Andrea Lattuada (VMware)
Generalized lemma broadcast, implements #37 (#1022)
committed

February 2024

Bryan Parno
Merge pull request #1004 from verus-lang/apply-verusfmt
committed