FStarLang / pulse

The Pulse separation logic DSL for F*
Apache License 2.0
6 stars 7 forks source link

In-place merge sort for slices #248

Open tahina-pro opened 5 days ago

tahina-pro commented 5 days ago

This PR reorganizes the implementations of in-place merge sort:

tahina-pro commented 5 days ago

This PR also marks the element type argument of Pulse.Lib.ArrayPtr.ptr and Pulse.Lib.Slice.slice strictly positive. This is needed to use slices in recursive type definitions.