law dg_eq

lawful-fields@0.1.1.0 · proof_digits.bend:428

import Base

428# The digit byte put_dec writes is DG.
429law dg_eq:
430  for +n: U32
431  {U32.add(U32.mod(n, 10), 48) == DG(U32.to_nat(n)) : U32}