def facts_0

bendtorch-core@0.1.0.0 · src/tensor/axis_algebra.bend:2114

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

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