BendMlTensorArray.ASet.Facts: 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 1947-1955 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=1947&end_line=1955

import Base

# ASet.Facts: what one pass over the tree a proves, for any n, j, v, z (n need not be a's real size):
# 1. Array.size(a) is the pair (a, ASet.sz(a));
# 2. the pair the write's descent returns is (the written array, the old value);
# 3. Array.size of the written array is the pair (written array, its sz);
# 4. the written array has a's sz;
# 5. reading the written array along the same path gives v;
# 6. the pair the read returns is (its first component, its second).
def ASet.Facts(-T: Data, -a: Array<T>, -n: U32, -j: U32, -v: T, -z: Bool) -> Type:
  {(a, ASet.sz(T, a)) == Array.size(T, a) : Array<T> & U32} & {(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} & {(ASet.NA(T, a, n, j, v, z), ASet.sz(T, ASet.NA(T, a, n, j, v, z))) == Array.size(T, ASet.NA(T, a, n, j, v, z)) : Array<T> & U32} & {ASet.sz(T, ASet.NA(T, a, n, j, v, z)) == ASet.sz(T, a) : U32} & {Pair.snd(Array<T>, T, ASet.K(T, a, n, j, v, z)) == v : T} & {(Pair.fst(Array<T>, T, ASet.K(T, a, n, j, v, z)), Pair.snd(Array<T>, T, ASet.K(T, a, n, j, v, z))) == ASet.K(T, a, n, j, v, z) : Array<T> & T} & Unit

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  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.G
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ASet.K
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ASet.NA
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ASet.sz