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

Version history of source/vstd/set_lib.rs

September 2026

ddt
add lemmas to vstd::set_lib, about Set::to_seq (#1797)
committed

June 2026

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

March 2026

Baltasar Dinis
vstd: add set equality lemma based on injective_on (#2266)
committed
Chris Hawblitzel
Merge branch 'main' into make_spec_type
committed
Chris Hawblitzel (Microsoft)
Set build (#2216)
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 seq-lemmas-triggers
committed
Chris Hawblitzel
Merge branch 'main' into assoc-const1
committed

November 2025

Baltasar Dinis
set: add lemma to relate `disjoint` with an empty intersection (#1974)
committed
Baltasar Dinis
Add lemmas regarding the length of `Set::map` for non-injective `f` and for `Map::values` (#1970)
committed

August 2025

Xinyi Wan
Strengthen Set::lemma_map_size (#1860)
committed

July 2025

Bryan Parno
Prepare Verus-related crates for posting to crates.io (#1815)
committed

June 2025

Natalie Neamtu
Merge branch 'main' into zero-to-nat/docs-retreat-2025
committed
Chris Hawblitzel
Merge branch 'main' into loop-infer-base
committed
Andrea Lattuada
Merge pull request #1653 from verus-lang/proof-in-spec
committed
Chris Hawblitzel
Add proof blocks for recursive spec function termination checking
committed
Daniel Schoepe
Add additional `Set` functions and lemmas (#1701)
committed

March 2025

Andrea Lattuada
add the lemma added in 309a27b to the default broadcast use set (#1542)
committed
Luka Duranovic
Add axiom which states that subsets of finite sets are finite (#1515)
committed
Travis Hance
fix definition of Set::is_empty (#1526)
committed

February 2025

Matthias
Add model for vstd Set and prove its axioms
committed
Alex Bai
use broadcast for map/set/multiset_properties (#1443)
committed

January 2025

Matthias
New (in-)finiteness lemmas for sets
committed

October 2024

Andrea Lattuada
warn that `assert forall |...| p ==> q` does not assume the antecedent
committed

August 2024

Chris Hawblitzel (Microsoft)
Prune broadcast functions based on their triggers (#1175)
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
verusfmt
committed
Andrea Lattuada
apply generalized broadcast to vstd
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
verusfmt
Format vstd with `verusfmt` version 0.2.3
committed
Andrea Lattuada
rename pervasive -> vstd
committed