law AL

lawful-fields@0.1.1.0 · proof_digits.bend:680

import Base
import lawful-bytes@0.1.1.0/defs.bend as D
import lawful-fields@0.1.1.0/fields.bend as FC

680law AL:
681  for +k: Nat
682  for +small: Bool
683  for +n: U32
684  for +acc: List<&2, U32>
685  for +hs: {U32.is_lt(n, 10) == small : Bool}
686  for +hacc: {D.all_bytes(acc) == True{} : Bool}
687  {D.all_bytes(FC.put_dec.digits(k, small, n, acc)) == True{} : Bool}