def axis_zero
bendtorch-core@0.1.0.0 · src/autograd/reduce_fiber_proof.bend:359
import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as ReduceFiberProof
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
359def axis_zero(+rh: Nat, +oh: Nat, axis: Shape.Axis<0n, rh, oh>) -> {oh == 0n : Nat}:
360 match axis:
361 case Shape.AxisEqual{left_eq, right_eq}:
362 left_eq
363 case Shape.AxisLeftOne{one, right_eq}:
364 Empty.absurd({oh == 0n : Nat}, Arith.clash(Equal.cong(Nat, Bool, n => Nat.is_eq(n, 0n), 1n, 0n, one)))
365 case Shape.AxisRightOne{left_eq, one}:
366 left_eq