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

Version history of source/vstd/seq.rs

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
Chris Hawblitzel (Microsoft)
Spec index range syntax (#2913)
committed

July 2026

Travis Hance
improve group_seq_axioms deprecation message (#2684)
committed
Baltasar Dinis
vstd: remove usage of group_seq_axioms and added axioms (#2678)
committed
Baltasar Dinis
vstd: finish proving lemmas for `Seq` (#2669)
committed
Baltasar Dinis
vstd: change Seq to Enum and verify axioms (#2625)
committed

May 2026

Chris Hawblitzel (Microsoft)
Add trait bound to spec == operator to improve type inference (#2377)
committed
Travis Hance
mark Seq as tracked so &mut Seq can be used (#2415)
committed
Travis Hance
update vstd to use the new_mut_ref style (#2408)
committed

March 2026

Chris Hawblitzel
Merge branch 'main' into ieee-float
committed
Chris Hawblitzel
Merge branch 'main' into metasized_sized_fix
committed
Bryan Parno
Update the seq! macro so that it doesn't treat `seq![1,]` as a two-element sequence.(#2227)
committed
Chris Hawblitzel
Merge branch 'main' into make_spec_type
committed

February 2026

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

December 2025

Travis Hance
warn about implicit mut-deref in spec equality (#2041)
committed
Chris Hawblitzel
Merge branch 'main' into dyn
committed
Chris Hawblitzel (Microsoft)
Merge pull request #2006 from verus-lang/seq-lemmas-triggers
committed

November 2025

Chris Hawblitzel
Add lemma_seq_two_subranges_index and group_seq_lemmas_expensive
committed

July 2025

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

May 2025

Nickolai Zeldovich
add Seq::tracked_pop_front() (#1659)
committed
Travis Hance
Add an 'axiom' keyword (#1518)
committed
Alex Bai
update syntax for broadcast use (#1571)
committed

April 2025

ziqiaozhou
Add tracked functions for Seq (#1596)
committed

March 2025

Andrea Lattuada
uninterp marker on uniterpreted spec fns (#1473)
committed

January 2025

Travis Hance
vstd: remove deprecated stuff
committed

October 2024

Bryan Parno
Represent large sequence literals using the recently added ArrayLiteral support (#1317)
committed

August 2024

Chris Hawblitzel (Microsoft)
Prune broadcast functions based on their triggers (#1175)
committed
Chris Hawblitzel
Fix axiom_seq_len_decreases (thanks to tjhance for pointing out the problem)
committed
Chris Hawblitzel
More decreases axioms for Vec and Seq (related to https://github.com/verus-lang/verus/issues/1222 )
committed

June 2024

Jay Bosamiya (Microsoft)
Implement repeat for the seq macro (#1178)
committed
Andrea Lattuada
Merge pull request #1168 from XuhengLi/main
committed
Andrea Lattuada
use literal type annotations in seq examples instead
committed
XuhengLi
Fix missing type annotation in examples in vstd/seq.rs.
committed

May 2024

Travis Hance
put deprecated attrs in cfg_attr
committed
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
Travis Hance
use vargo for building verusdoc
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