BroadcastProofs.aligned_left: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as BroadcastProofs
Lines 43-64 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=43&end_line=64

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

def aligned_left(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +alignment: Shape.Aligned(left, right, output), +coordinate: Shape.Coordinate(output)) -> {Shape.indices(left, Shape.Aligned.project_left(left, right, output, alignment, coordinate)) == Shape.broadcast_indices(left, Shape.indices(output, coordinate)) : List<&2, Nat>}:
  match left right output:
    case Nil{} Nil{} Nil{}:
      {==}
    case +lh <> +lt +rh <> +rt +oh <> +ot:
      Shape.AStep{+axis, +tail} = alignment
      Shape.CStep{+index, +rest} = coordinate
      %aligned_left(lt, rt, ot, tail, rest) : {Shape.Fin.value(lh, Shape.Axis.project_left(lh, rh, oh, axis, index)) <> Shape.indices(lt, Shape.Aligned.project_left(lt, rt, ot, tail, rest)) == Shape.broadcast_index(lh, Shape.Fin.value(oh, index)) <> _ : List<&2, Nat>}
      %axis_left(lh, rh, oh, axis, index) : {Shape.Fin.value(lh, Shape.Axis.project_left(lh, rh, oh, axis, index)) <> Shape.indices(lt, Shape.Aligned.project_left(lt, rt, ot, tail, rest)) == _ <> Shape.indices(lt, Shape.Aligned.project_left(lt, rt, ot, tail, rest)) : List<&2, Nat>}
      {==}
    case Nil{} Nil{} oh <> ot:
      match alignment:
    case Nil{} rh <> rt Nil{}:
      match alignment:
    case lh <> lt Nil{} Nil{}:
      match alignment:
    case Nil{} rh <> rt oh <> ot:
      match alignment:
    case lh <> lt Nil{} oh <> ot:
      match alignment:
    case lh <> lt rh <> rt Nil{}:
      match alignment:

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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=axis_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Aligned
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Aligned.Step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Aligned.project_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Axis.project_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Coordinate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Coordinate.Step
  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
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=broadcast_indices
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=indices