AxisAlgebra.facts_0: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend as AxisAlgebra
Lines 2114-2120 of bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&start_line=2114&end_line=2120

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend as Axis

def facts_0(+axes: List<&2, Nat>, accepted: {True{} == Axis.valid(0n, axes) : Bool}) -> Facts<0n, axes>:
  match axes:
    case Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_empty(A, items, length),
        dims => length => product_empty(dims, length), dims => coords => dl => cl => fit_empty(dims, coords, dl, cl)}
    case +a0 <> +tail:
      Empty.absurd(Facts<0n, a0 <> tail>, Shape.clash(accepted))

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=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=clash
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=Facts
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_empty
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_empty
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_empty
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend&name=valid