law put_dec_view

lawful-fields@0.1.1.0 · LAWS.bend:108

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

108# put_dec writes n in decimal at the end (room for 10 more bytes needed).
109law put_dec_view:
110  for b: D.Bytes
111  for d: Nat
112  for n: U32
113  for h: {D.ok(b, d) == True{} : Bool}
114  for hc: {Nat.is_le(Nat.add(D.size(b), 10n), D.cap(b)) == True{} : Bool}
115  {D.view(C.put_dec(b, n)) == List.append(&2, U32, D.view(b), F.show(n)) : List<&2, U32>}