law get_go_eta

lawful-arrays@0.1.0.0 · proof_tree.bend:268

import lawful-arrays@0.1.0.0/proof_tree.bend as ProofTree
import Base

268law get_go_eta:
269  for -T: Data
270  for a: Array<T>
271  for +n: U32
272  for +i: U32
273  for +z: Bool
274  {Array.get.go(T, a, n, i, z) == (a, Pair.snd(Array<T>, T, Array.get.go(T, a, n, i, z))) : Array<T> & T}

Uses (13)

Used by (1)