BendMlTensorArray.ASet.Side: 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 2133-2136 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=2133&end_line=2136

import Base

# ASet.Side: what a pass over a subtree the write does not enter proves: Array.size(a) is (a, ASet.sz(a)), and the
# pair a read along (n, k, w) returns is (its first component, its second)
def ASet.Side(-T: Data, -a: Array<T>, -n: U32, -k: U32, -w: Bool) -> Type:
  {(a, ASet.sz(T, a)) == Array.size(T, a) : Array<T> & U32} & {(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} & Unit

Uses (11):
  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=Array.size
  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.sz