BroadcastProofs.axis_right: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as BroadcastProofs
Lines 31-41 of bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend&start_line=31&end_line=41

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

def axis_right(+left: Nat, +right: Nat, +output: Nat, +axis: Shape.Axis<left, right, output>, +index: Shape.Fin(output)) -> {Shape.Fin.value(right, Shape.Axis.project_right(left, right, output, axis, index)) == Shape.broadcast_index(right, Shape.Fin.value(output, index)) : Nat}:
  match axis:
    case Shape.AxisEqual{left_eq, right_eq}:
      %h@right_eq : {Shape.Fin.value(_, Shape.Axis.project_right(left, _, output, Shape.AxisEqual{left_eq, h}, index)) == Shape.broadcast_index(_, Shape.Fin.value(output, index)) : Nat}
      fin_broadcast(output, index)
    case Shape.AxisLeftOne{one, right_eq}:
      %h@right_eq : {Shape.Fin.value(_, Shape.Axis.project_right(left, _, output, Shape.AxisLeftOne{one, h}, index)) == Shape.broadcast_index(_, Shape.Fin.value(output, index)) : Nat}
      fin_broadcast(output, index)
    case Shape.AxisRightOne{left_eq, one}:
      %h@one : {Shape.Fin.value(_, Shape.Axis.project_right(left, _, output, Shape.AxisRightOne{left_eq, h}, index)) == Shape.broadcast_index(_, Shape.Fin.value(output, index)) : Nat}
      {==}

Uses (7):
  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/broadcast_proofs.bend&name=fin_broadcast
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Axis
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Axis.project_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=broadcast_index