law at_view

lawful-bytes@0.1.1.0 · LAWS.bend:67

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

67law at_view:
68  for b: D.Bytes
69  for d: Nat
70  for i: U32
71  for h: {D.ok(b, d) == True{} : Bool}
72  for hi: {Nat.is_lt(U32.to_nat(i), D.size(b)) == True{} : Bool}
73  {Some{Pair.snd(D.Bytes, U32, B.at(b, i))} == List.get(&2, U32, D.view(b), U32.to_nat(i)) : Maybe<&2, U32>}