def wok_i

bend-kit-collections@0.1.4.1 · nat_order.bend:20

import Base
import bend-mathlib@0.7.4.0/bool.bend as MBool

20def wok_i(+wl: Nat, +wh: Nat, el: {Nat.is_le(wh, mul3(wl)) == True{} : Bool},
21  er: {Nat.is_le(wl, mul3(wh)) == True{} : Bool}) -> {wok(wl, wh) == True{} : Bool}:
22  MBool.and_eq_true(Nat.is_le(wh, mul3(wl)), Nat.is_le(wl, mul3(wh)), el, er)