Flat.left_bound: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/flat.bend as Flat
Lines 12-26 of bendtorch-core@0.1.0.0/src/shape/flat.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/flat.bend&start_line=12&end_line=26

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/shape/coordinate_proofs.bend as Coordinates
import bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend as Projection

def left_bound(+plan: Shape.BroadcastPlan, -rows: List<&2, Shape.Row>, exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>}, +value: Nat, bound: {True{} == Nat.is_lt(value, Shape.elements(Shape.output_shape(plan))) : Bool}) -> {True{} == Nat.is_lt(Shape.walk_left(rows, value), Shape.elements(Shape.left_shape(plan))) : Bool}:
  +left = Shape.extents(Shape.left_shape(plan))
  +right = Shape.extents(Shape.right_shape(plan))
  +output = Shape.extents(Shape.output_shape(plan))
  +input = Shape.left_shape(plan)
  +fits = Coordinates.size_fits(Shape.output_shape(plan), value, bound)
  +index = Coordinates.fin_from(Shape.numel(output), value, fits)
  +projected = Shape.project_left(left, right, output, Shape.alignment(plan), Shape.unflatten(output, index))
  +table = Shape.index_table(left, right, output)
  %Equal.sym(List<&2, Shape.Row>, rows, table, exact) : {True{} == Nat.is_lt(Shape.walk_left(_, value), Shape.elements(input)) : Bool}
  %Coordinates.fin_from_value(Shape.numel(output), value, fits) : {True{} == Nat.is_lt(Shape.walk_left(table, _), Shape.elements(input)) : Bool}
  %Equal.sym(Nat, Shape.walk_left(table, Shape.Fin.value(Shape.numel(output), index)), Shape.row_major(Shape.extents(input), projected), Projection.walk_left_value(left, right, output, Shape.alignment(plan), index)) : {True{} == Nat.is_lt(_, Shape.elements(input)) : Bool}
  %Equal.sym(Nat, Shape.elements(input), Shape.numel(Shape.extents(input)), Shape.elements_exact(input)) : {True{} == Nat.is_lt(Shape.row_major(Shape.extents(input), projected), _) : Bool}
  %Nats.lt_true(Shape.row_major(Shape.extents(input), projected), Shape.numel(Shape.extents(input)), Coordinates.row_major_lt(Shape.extents(input), projected)) : {True{} == _ : Bool}
  {==}

Uses (27):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=fin_from
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=fin_from_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=row_major_lt
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=size_fits
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BroadcastPlan
  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=Row
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=alignment
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=elements
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=elements_exact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=extents
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=index_table
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=left_shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=output_shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=project_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=right_shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=row_major
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=unflatten
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=walk_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=lt_true
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&name=walk_left_value