Function vstd::relations::sorted_by

source · 
pub open spec fn sorted_by<T>(a: Seq<T>, less_than: FnSpec<(T, T), bool>) -> bool
Expand description
{ forall |i: int, j: int| 0 <= i < j < a.len() ==> #[trigger] less_than(a[i], a[j]) }

This function returns true if the input sequence a is sorted, using the input function less_than to sort the elements