~/jendhub

def pair_equal

bendtorch-core@0.1.0.0 · src/tensor/elementwise_parallel_proof.bend:104

import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as ElementwiseParallelProof
import Base

104def pair_equal(-a: Array<F32>, -b: Array<F32>, -A: Array<F32>, -B: Array<F32>, ea: {a == A : Array<F32>}, eb: {b == B : Array<F32>}) ->
105  {(a, b) == (A, B) : Array<F32> & Array<F32>}:
106  Equal.trans(Array<F32> & Array<F32>, (a, b), (A, b), (A, B),
107    Equal.cong(Array<F32>, Array<F32> & Array<F32>, x => (x, b), a, A, ea),
108    Equal.cong(Array<F32>, Array<F32> & Array<F32>, y => (A, y), b, B, eb))

Uses (6)

Used by (8)