law get_new_go

lawful-arrays@0.1.0.0 · proof_tree.bend:221

import Base

221law get_new_go:
222  for -T: Data
223  for +d: Nat
224  for +v: T
225  for +n: U32
226  for +i: U32
227  for +z: Bool
228  {Pair.snd(Array<T>, T, Array.get.go(T, Array.new(T, d, v), n, i, z)) == v : T}