law insert_count

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

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

198law insert_count:
199  for ~A: Data
200  for ~o: C.Ord<A>
201  for ~eq: A -> A -> Bool
202  for +y: A
203  for +x: A
204  for xs: List<&2, A>
205  {bump(eq(y, x), count(~A, ~eq, y, xs)) == count(~A, ~eq, y, insert(~A, ~o, x, xs)) : Nat}