BendMlTensorArray.ASet.Reads: def of bend-ml-tensor-array@0.1.19.0
Import: import bend-ml-tensor-array@0.1.19.0/main.bend as BendMlTensorArray
Lines 2169-2175 of bend-ml-tensor-array@0.1.19.0/main.bend: https://jend.leeeet.dev/read.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&start_line=2169&end_line=2175

import Base

# ASet.Reads: what one pass over the tree a proves about a write along (n, j, v, z) and a read along (n, k, w):
# 1. the pair the write's descent returns is (the written array, the old value);
# 2. the read of a returns a pair (first component, second);
# 3. so does the read of the written array;
# 4. if the descents split, the read finds the same value in the written array as in a.
def ASet.Reads(-T: Data, -a: Array<T>, -n: U32, -j: U32, -v: T, -z: Bool, -k: U32, -w: Bool) -> Type:
  {(ASet.NA(T, a, n, j, v, z), Pair.snd(Array<T>, T, ASet.G(T, a, n, j, v, z))) == ASet.G(T, a, n, j, v, z) : Array<T> & T} & {(Pair.fst(Array<T>, T, Array.get.go(T, a, n, k, w)), Pair.snd(Array<T>, T, Array.get.go(T, a, n, k, w))) == Array.get.go(T, a, n, k, w) : Array<T> & T} & {(Pair.fst(Array<T>, T, Array.get.go(T, ASet.NA(T, a, n, j, v, z), n, k, w)), Pair.snd(Array<T>, T, Array.get.go(T, ASet.NA(T, a, n, j, v, z), n, k, w))) == Array.get.go(T, ASet.NA(T, a, n, j, v, z), n, k, w) : Array<T> & T} & (ASet.Apart(T, a, n, j, z, k, w) -> {Pair.snd(Array<T>, T, Array.get.go(T, ASet.NA(T, a, n, j, v, z), n, k, w)) == Pair.snd(Array<T>, T, Array.get.go(T, a, n, k, w)) : T}) & Unit

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.fst
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ASet.Apart
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ASet.G
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ASet.NA