def axis_left

bendtorch-core@0.1.0.0 · src/shape/broadcast_proofs.bend:19

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

19def axis_left(+left: Nat, +right: Nat, +output: Nat, +axis: Shape.Axis<left, right, output>, +index: Shape.Fin(output)) -> {Shape.Fin.value(left, Shape.Axis.project_left(left, right, output, axis, index)) == Shape.broadcast_index(left, Shape.Fin.value(output, index)) : Nat}:
20  match axis:
21    case Shape.AxisEqual{left_eq, right_eq}:
22      %h@left_eq : {Shape.Fin.value(_, Shape.Axis.project_left(_, right, output, Shape.AxisEqual{h, right_eq}, index)) == Shape.broadcast_index(_, Shape.Fin.value(output, index)) : Nat}
23      fin_broadcast(output, index)
24    case Shape.AxisLeftOne{one, right_eq}:
25      %h@one : {Shape.Fin.value(_, Shape.Axis.project_left(_, right, output, Shape.AxisLeftOne{h, right_eq}, index)) == Shape.broadcast_index(_, Shape.Fin.value(output, index)) : Nat}
26      {==}
27    case Shape.AxisRightOne{left_eq, one}:
28      %h@left_eq : {Shape.Fin.value(_, Shape.Axis.project_left(_, right, output, Shape.AxisRightOne{h, one}, index)) == Shape.broadcast_index(_, Shape.Fin.value(output, index)) : Nat}
29      fin_broadcast(output, index)