law dg_small

lawful-fields@0.1.1.0 · proof_digits.bend:468

import Base

468law dg_small:
469  for +n: U32
470  for +hs: {U32.is_lt(n, 10) == True{} : Bool}
471  {U32.add(n, 48) == DG(U32.to_nat(n)) : U32}