SumDimsLAWS.sum_dims_rank_limit: 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 104-107 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=104&end_line=107

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/autograd/sum_dims.bend as SumDims

law sum_dims_rank_limit:
  for +extent: U32
  for +rest: List<&2, U32>
  {SumDims.limit(extent <> rest) == U32.from_nat(Shape.rank_dimensions(extent <> rest)) : U32}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/sum_dims.bend&name=limit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=rank_dimensions