def frozen_nt_unsent

bendtorch-core@0.1.0.0 · src/autograd/tensor_backward_PROOF.bend:68

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend as Backward

68def frozen_nt_unsent(+id: Nat, +a: Nat, +b: Nat, +left: Shape.Shape, +right: Shape.Shape, saved: Backward.Saved, g: Core.Dynamic,
69  computed: {Bool.and(Nat.is_eq(id, a), Bool.not(Nat.is_eq(id, b))) == False{} : Bool}) ->
70  {Backward.nt_frozen(id, a, b, left, right, saved, g, Bool.and(Nat.is_eq(id, a), Bool.not(Nat.is_eq(id, b)))) ==
71    Backward.unsent(id, Backward.vjp_matmul_nt(a, b, left, right, saved, g)) : Backward.Pass}:
72  %Equal.sym(Bool, Bool.and(Nat.is_eq(id, a), Bool.not(Nat.is_eq(id, b))), False{}, computed) :
73    {Backward.nt_frozen(id, a, b, left, right, saved, g, _) == Backward.unsent(id, Backward.vjp_matmul_nt(a, b, left, right, saved, g)) : Backward.Pass}
74  {==}