def bounded_failure

bendtorch-core@0.1.0.0 · src/tensor/permute_contract.bend:81

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout

81def bounded_failure(+input: Shape.Shape, +axes: List<&2, U32>, decision: Shape.BoolCase<Layout.bounded(axes, Shape.rank(input))>,
82  outside: {Layout.bounded(axes, Shape.rank(input)) == False{} : Bool}) ->
83  {Layout.plan_bounded(input, axes, decision) == Fail{Layout.AxisOutOfBounds{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
84  match decision:
85    case Shape.BFalse{no}:
86      {==}
87    case Shape.BTrue{yes}:
88      Empty.absurd({Layout.plan_bounded(input, axes, Shape.BTrue{yes}) == Fail{Layout.AxisOutOfBounds{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>},
89        Nats.contradiction(Layout.bounded(axes, Shape.rank(input)), yes, Equal.sym(Bool, Layout.bounded(axes, Shape.rank(input)), False{}, outside)))