def bv_le
import bend-collections-laws-math@1.0.0.0/proofs/math/random/bits.bend as Bitsimport Base
53def bv_le(+b: Bool) -> {Nat.is_le(bv(b), 1n) == True{} : Bool}:
54 match b:
55 case True{}:
56 {==}
57 case False{}:
58 {==}
import bend-collections-laws-math@1.0.0.0/proofs/math/random/bits.bend as Bitsimport Base
53def bv_le(+b: Bool) -> {Nat.is_le(bv(b), 1n) == True{} : Bool}:
54 match b:
55 case True{}:
56 {==}
57 case False{}:
58 {==}