law decb_fits

lawful-fields@0.1.1.0 · LAWS.bend:169

import Base
import lawful-fields@0.1.1.0/defs.bend as F

169# decb (with bound 2^32) is dec when the number fits.
170law decb_fits:
171  for xs: List<&2, U32>
172  for n: Nat
173  for h: {F.dec(xs) == Some{n} : Maybe<&2, Nat>}
174  for hn: {Nat.is_lt(n, Nat.pow(2n, 32n)) == True{} : Bool}
175  {F.decb(xs, Nat.pow(2n, 32n)) == Some{n} : Maybe<&2, Nat>}