make example more clear and add to documentation

source/pervasive/seq_lib.rs

@@ -13,8 +13,6 @@ use crate::set_lib::lemma_set_properties;
 use crate::multiset::Multiset;
 #[allow(unused_imports)]
 use crate::relations::*;
-// use crate::seq_merge_sort::lemma_merge_sorted_with_ensures;
-// use crate::seq_merge_sort::merge_sorted_with;
 
 verus! {
 
@@ -69,6 +67,12 @@ impl<A> Seq<A> {
     }
 
     /// Sorts the sequence according to the given leq function
+    /// 
+    /// ## Example
+    /// 
+    /// ```rust
+    /// {{#include ../../../rust_verify/example/multiset.rs:sorted_by_eg}}
+    /// ```
     pub open spec fn sort_by(self, leq: FnSpec(A,A) ->bool) -> Seq<A>
         recommends
             total_ordering(leq),

source/rust_verify/example/multiset.rs

@@ -24,26 +24,26 @@ proof fn multiset_ext_eq2() {
 }
 
 proof fn sorted_by_eg() {
+    //Provides the verifier with important lemmas about sequences
+    lemma_seq_properties::<int>();
 
     let leq = |x: int, y: int| x <= y;
 
-    let unsorted = seq![3, 1, 2];
+    let unsorted = seq![3, 1, 5, 2, 4];
     let sorted = unsorted.sort_by(leq);
+
+    //Tells the verifier what the sort_by function ensures to be true
+    lemma_sort_by_ensures::<int>(unsorted, leq); 
+
+    let expected_result: Seq<int> = seq![1, 2, 3, 4, 5];
+    assert(sorted_by(expected_result,leq));
+
+    assert(expected_result.to_multiset() =~= unsorted.to_multiset());
+
+    //Proves that any two sequences that are sorted and have the same elements are equal.
+    lemma_sorted_unique(expected_result, unsorted.sort_by(leq), leq);
 
-    let result: Seq<int> = seq![1, 2, 3];
-
-    lemma_sort_by_ensures::<int>(unsorted, leq);
-    lemma_sort_by_ensures::<int>(result, leq);
-    lemma_seq_properties::<int>();
-
-    assert(sorted_by(result,leq));
-
-    assert(result =~= (unsorted.sort_by(leq))) by {
-        assert(result.to_multiset() =~= unsorted.to_multiset());
-        lemma_sorted_unique(result, unsorted.sort_by(leq), leq);
-    };
-
-    assert(sorted =~= result);
+    assert(sorted =~= expected_result);
 }
 
 }