SumDimsLAWS.sum_dims_duplicate_axis: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/sum_dims_LAWS.bend as SumDimsLAWS
Lines 117-122 of bendtorch-core@0.1.0.0/src/autograd/sum_dims_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/sum_dims_LAWS.bend&start_line=117&end_line=122

import Base
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/autograd/sum_dims.bend as SumDims

law sum_dims_duplicate_axis:
  for +axes: List<&2, U32>
  for +limit: U32
  for inside: {Layout.bounded(axes, limit) == True{} : Bool}
  for repeated: {Layout.unique(axes) == False{} : Bool}
  {SumDims.refusal(axes, limit) == Some{Layout.DuplicateAxis{}} : Maybe<&2, Layout.Error>}

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/sum_dims.bend&name=refusal
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/sum_dims.bend&name=refused
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=bounded
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=unique