law get_view

lawful-arrays@0.1.0.0 · LAWS.bend:58

import Base
import lawful-arrays@0.1.0.0/defs.bend as D

58# Array.get reads leaf i (modulo the size).
59law get_view:
60  for -T: Data
61  for a: Array<T>
62  for d: Nat
63  for i: U32
64  for hf: {D.full(T, a, d) == True{} : Bool}
65  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
66  {Some{Pair.snd(Array<T>, T, Array.get(T, a, i))} == List.get(&2, T, D.view(T, a), D.slot(i, d)) : Maybe<&2, T>}