law byte_lt

lawful-words@0.1.0.0 · proof_bytes.bend:559

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

559law byte_lt:
560  for +w: U32
561  for +j: Nat
562  {U32.is_lt(D.byte(w, j), 256) == True{} : Bool}

Uses (16)

Used by (5)