law decb_fits

lawful-fields@0.1.1.0 · proof_list.bend:464

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

464law decb_fits:
465  for +xs: List<&2, U32>
466  for +n: Nat
467  for +h: {F.dec(xs) == Some{n} : Maybe<&2, Nat>}
468  for +hn: {Nat.is_lt(n, Nat.pow(2n, 32n)) == True{} : Bool}
469  {F.decb(xs, Nat.pow(2n, 32n)) == Some{n} : Maybe<&2, Nat>}