Should destructuring be expanded to provide more intuitive syntax for programs that can be syntactically proven to be total?

[loreanvictor]

Look at this gist. Both quick sort and merge sort are written in relatively intuitive and convenient forms, however due to limitations of our destructuring syntax (as is), only quick sort can be syntactically proven to be total.

Since Kāshi is to be used for configuration, syntactic checking for totality is a desirable configuration for some implementations of the language. Merge sort is obviously total, so maybe we can extend our destructuring syntax so that it would have an intuitive expression in Kāshi that can also syntactically be proven to be total?