TensorVjpPROOF.factors_snoc: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend as TensorVjpPROOF
Lines 289-299 of bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend&start_line=289&end_line=299

import Base
import bendtorch-core@0.1.0.0/src/tensor/dot_fold.bend as DotFold

def factors_snoc(+before: List<&2, DotFold.Factors>, +after: List<&2, DotFold.Factors>, +x: F32, +y: F32, +u: F32, +v: F32,
  rest: {before == after : List<&2, DotFold.Factors>}, xu: {x == u : F32}, yv: {y == v : F32}) ->
  {List.append(&2, DotFold.Factors, before, [DotFold.Factors{x, y}]) ==
    List.append(&2, DotFold.Factors, after, [DotFold.Factors{u, v}]) : List<&2, DotFold.Factors>}:
  %rest : {List.append(&2, DotFold.Factors, before, [DotFold.Factors{x, y}]) ==
    List.append(&2, DotFold.Factors, _, [DotFold.Factors{u, v}]) : List<&2, DotFold.Factors>}
  %xu : {List.append(&2, DotFold.Factors, before, [DotFold.Factors{x, y}]) ==
    List.append(&2, DotFold.Factors, before, [DotFold.Factors{_, v}]) : List<&2, DotFold.Factors>}
  %yv : {List.append(&2, DotFold.Factors, before, [DotFold.Factors{x, y}]) ==
    List.append(&2, DotFold.Factors, before, [DotFold.Factors{x, _}]) : List<&2, DotFold.Factors>}
  {==}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/dot_fold.bend&name=Factors