law model_get

bend-osdev-array@0.1.0.1 · LAWS.bend:94

import Base
import bend-osdev-array@0.1.0.1/array.bend as A

94law model_get:
95  for -T: Data
96  for d: Nat
97  for a: Array<T>
98  for h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}
99  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
100  for i: U32
101  {List.get(&2, T, A.Arrays.leaves(T, a), A.Arrays.index(d, i)) == Some{Pair.snd(Array<T>, T, Array.get(T, a, i))} : Maybe<&2, T>}