law ne_dec

lawful-fields@0.1.1.0 · proof_digits.bend:90

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

90law ne_dec:
91  for +ys: List<&2, U32>
92  for +h: {Nat.is_lt(0n, List.length(&2, U32, ys)) == True{} : Bool}
93  {Maybe.is_some(&2, Nat, F.dec(ys)) == alld(ys) : Bool}