law unpack_get0

lawful-bytes@0.1.1.0 · proof_core.bend:72

import Base
import lawful-bytes@0.1.1.0/defs.bend as D
import lawful-words@0.1.0.0/defs.bend as W

72law unpack_get0:
73  for +w: U32
74  for +t: List<&2, U32>
75  for +r: Nat
76  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
77  {List.get(&2, U32, D.unpack(w <> t), r) == Some{W.byte(w, r)} : Maybe<&2, U32>}