def triple
bendtorch-core@0.1.0.0 · src/tensor/gather_PROOF.bend:459
import bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend as GatherPROOF
import Base
459def triple(-acc: F32, -x: F32, -a: Array<F32>, -b: Array<U32>, -A: Array<F32>, -B: Array<U32>, ea: {a == A : Array<F32>}, eb: {b == B : Array<U32>}) ->
460 {(F32.add(acc, x), (a, b)) == (F32.add(acc, x), (A, B)) : F32 & (Array<F32> & Array<U32>)}:
461 Equal.cong(Array<F32> & Array<U32>, F32 & (Array<F32> & Array<U32>), p => (F32.add(acc, x), p), (a, b), (A, B), both(a, b, A, B, ea, eb))