enrich arr2list , 
       intnat
 with
   procedures 
      swap#  int × int : array nonfunctional;
      two_way_sort#   : array nonfunctional;
declaration 
   swap-decl : swap# (i, j; ar)
                 { 
                    let bv = ar[i→n(i)] in { 
                                              ar := ar[i→n(i), ar[i→n(j)]] ; ar := ar[i→n(j), bv]
                                           }
                 };
   two_way_sort-decl
   : two_way_sort# (;ar)
       { 
          let i = 0, j = n→i(# ar) - 1
          in while i ≤ j do if ¬ ar[i→n(i)]
                            then i := i + 1
                            else if ar[i→n(j)]
                                 then j := j - 1
                                 else { 
                                         swap#(i, j; ar) ; i := i + 1 ; j := j - 1
                                      }
       };
end enrich