ReduceParallelProof.next_same: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend as ReduceParallelProof
Lines 547-553 of bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&start_line=547&end_line=553

import Base
import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce

# Two closures equal on every argument continue a pair alike.
def next_same(-fast: F32 -> Array<F32> -> F32 & Array<F32>, -slow: F32 -> Array<F32> -> F32 & Array<F32>,
  same: @value: F32 -> @array: Array<F32> -> Generic.Fact<{fast(value, array) == slow(value, array) : F32 & Array<F32>}>,
  pair: F32 & Array<F32>) -> Generic.Fact<{Reduce.walk_next(fast, pair) == Reduce.walk_next(slow, pair) : F32 & Array<F32>}>:
  match pair:
    case Tuple{value, array}:
      same(value, array)

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=walk_next
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Fact