BinaryProofs.scalar_cong: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs.bend as BinaryProofs
Lines 227-231 of bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs.bend&start_line=227&end_line=231

import Base
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise

def scalar_cong(+operation: Elementwise.Operation, -x: F32, -y: F32, -u: F32, -v: F32, ex: {x == y : F32}, eu: {u == v : F32}) ->
  {Elementwise.scalar(operation, x, u) == Elementwise.scalar(operation, y, v) : F32}:
  %ex : {Elementwise.scalar(operation, x, u) == Elementwise.scalar(operation, _, v) : F32}
  %eu : {Elementwise.scalar(operation, x, u) == Elementwise.scalar(operation, x, _) : F32}
  {==}

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Operation
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=scalar