Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
The `MergeSort` function is in the hot path. The slice (x[1..]) operation is not optimized in Dafny. This optimizes this function by turning the recursive slice into a loop over an index into the seq. Further, a bounded integer version is also included. It also limits the total amount of data copied.
- Loading branch information