CoordinateProofs.indices_of: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as CoordinateProofs
Lines 55-67 of bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&start_line=55&end_line=67

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

def indices_of(+dims: List<&2, Nat>, +values: List<&2, Nat>, +fits: Fits(dims, values)) -> {Shape.indices(dims, coordinate_of(dims, values, fits)) == values : List<&2, Nat>}:
  match dims values:
    case Nil{} Nil{}:
      {==}
    case +dh <> +dt +vh <> +vt:
      FStep{+bound, +tail} = fits
      %Equal.sym(Nat, Shape.Fin.value(dh, fin_from(dh, vh, bound)), vh, fin_from_value(dh, vh, bound)) : {_ <> Shape.indices(dt, coordinate_of(dt, vt, tail)) == vh <> vt : List<&2, Nat>}
      %Equal.sym(List<&2, Nat>, Shape.indices(dt, coordinate_of(dt, vt, tail)), vt, indices_of(dt, vt, tail)) : {vh <> _ == vh <> vt : List<&2, Nat>}
      {==}
    case Nil{} vh <> vt:
      match fits:
    case dh <> dt Nil{}:
      match fits:

Uses (10):
  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=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=Fits
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=Fits.Step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=coordinate_of
  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/core.bend&name=Fin.value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=indices