~/jendhub

def ASet.Copy

bend-ml-tensor-array@0.1.19.0 · main.bend:2005

import bend-ml-tensor-array@0.1.19.0/main.bend as BendMlTensorArray
import Base

2005# ASet.copy(T, a): one pass over a hands back the same array b, its size n as a value, and the facts
2006# that tie them to a: b is a, n is ASet.sz(T, b), and Array.size(b) is the pair (b, ASet.sz(T, b))
2007def ASet.Copy(-T: Data, -a: Array<T>) -> Type:
2008  &b: Array<T> -> &n: U32 -> {b == a : Array<T>} & {n == ASet.sz(T, b) : U32} & {(b, ASet.sz(T, b)) == Array.size(T, b) : Array<T> & U32} & Unit

Uses (8)

Used by (5)