def pair_nats

bendtorch-core@0.1.0.0 · src/tensor/batched_matmul_PROOF.bend:712

import Base

712def 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>}:
713  %Equal.sym(Nat, a, c, ac) : {[_, b] == [c, d] : List<&2, Nat>}
714  %Equal.sym(Nat, b, d, bd) : {[c, _] == [c, d] : List<&2, Nat>}
715  {==}