def g_heavy_hi

bend-kit-collections@0.1.4.1 · LAWS.bend:275

import Base
import bend-kit-collections@0.1.4.1/omap.bend as O

275# The ghost map below has the shape of OMap: it builds nodes with the same
276# OMap.bin and rotations, but it compares Nat weights where OMap compares U32
277# sizes. While 3 * (size + 1) stays below 2^32, the U32 tests give the same
278# answers, so g_put and g_del give the same tree as put and del. The checker
279# cannot see into U32, so that link is an assumption, checked on fixtures below.
280def g_heavy_hi(-K: Data, -V: Data, +lo: O.OMap<K, V>, +hi: O.OMap<K, V>) -> Bool:
281  Nat.is_gt(omap_weight(K, V, hi), Nat.mul(3n, omap_weight(K, V, lo)))