law bit_ge32

lawful-words@0.1.0.0 · proof_bytes.bend:96

import Base
import lawful-words@0.1.0.0/defs.bend as D

96law bit_ge32:
97  for +a: U32
98  for +k: Nat
99  for +hk: {Nat.is_le(32n, k) == True{} : Bool}
100  {D.bit(a, k) == False{} : Bool}