BatchedMatmulPROOF.pair_nats: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend as BatchedMatmulPROOF
Lines 712-715 of bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&start_line=712&end_line=715

import Base

def pair_nats(+a: Nat, +b: Nat, +c: Nat, +d: Nat, +ac: {a == c : Nat}, +bd: {b == d : Nat}) -> {[a, b] == [c, d] : List<&2, Nat>}:
  %Equal.sym(Nat, a, c, ac) : {[_, b] == [c, d] : List<&2, Nat>}
  %Equal.sym(Nat, b, d, bd) : {[c, _] == [c, d] : List<&2, Nat>}
  {==}

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat