law dtop

lawful-fields@0.1.1.0 · proof_digits.bend:170

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

170# The start test of digits against the slice it reads.
171law dtop:
172  for +n: Nat
173  for +from: U32
174  for +to: U32
175  for +xs: List<&2, U32>
176  for +hn: {Nat.sub(U32.to_nat(to), U32.to_nat(from)) == n : Nat}
177  for +hle: {Nat.is_le(U32.to_nat(from), U32.to_nat(to)) == True{} : Bool}
178  for +hlen: {Nat.is_le(Nat.add(U32.to_nat(from), n), List.length(&2, U32, xs)) == True{} : Bool}
179  {Bool.and(U32.is_lt(from, to), alld(D.slice(xs, U32.to_nat(from), n))) == Maybe.is_some(&2, Nat, F.dec(D.slice(xs, U32.to_nat(from), n))) : Bool}