law digits_view

lawful-fields@0.1.1.0 · LAWS.bend:90

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

90# digits says the bytes are one or more decimal digits, a number of any size
91# (num answers None both for non-numbers and for numbers of 2^32 or more).
92law digits_view:
93  for b: D.Bytes
94  for d: Nat
95  for from: U32
96  for to: U32
97  for h: {D.ok(b, d) == True{} : Bool}
98  for hft: {U32.is_le(from, to) == True{} : Bool}
99  for ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}
100  {Pair.snd(D.Bytes, Bool, C.digits(b, from, to)) == F.all_digits(D.slice(D.view(b), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from)))) : Bool}