law go_some

lawful-fields@0.1.1.0 · proof_digits.bend:71

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

71# dec.go keeps a value exactly while every byte is a digit.
72law go_some:
73  for +ys: List<&2, U32>
74  for +m: Maybe<&2, Nat>
75  {Maybe.is_some(&2, Nat, F.dec.go(ys, m)) == Bool.and(Maybe.is_some(&2, Nat, m), alld(ys)) : Bool}