def bv_le

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/bits.bend:53

import 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      {==}