broadcast use vstd axioms and lemmas for new pcm_lib

verus-lang · Apr 25, 2024 · 7244402 · 7244402
1 parent 88a933a
commit 7244402
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/source/vstd/pcm_lib.rs b/source/vstd/pcm_lib.rs
@@ -13,7 +13,9 @@ use builtin_macros::*;
 
 verus! {
 
+broadcast use crate::vstd_default;
 /// Combines a list of values into one value using P::op().
+
 pub open spec fn combine_values<P: PCM>(values: Seq<P>) -> P
     decreases values.len(),
 {