law sort_count

bend-lawful-stdlib@0.1.0.0 · src/sorted.bend:215

import Base
import bend-lawful-stdlib@0.1.0.0/src/class.bend as C

215# sort keeps every element's count.
216law sort_count:
217  for ~A: Data
218  for ~o: C.Ord<A>
219  for ~eq: A -> A -> Bool
220  for +y: A
221  for xs: List<&2, A>
222  {count(~A, ~eq, y, xs) == count(~A, ~eq, y, sort(~A, ~o, xs)) : Nat}