CoordinateProofs.offset_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 89-91 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=89&end_line=91

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

def offset_of(+dims: List<&2, Nat>, +values: List<&2, Nat>, +fits: Fits(dims, values)) -> {Shape.row_major(dims, coordinate_of(dims, values, fits)) == Shape.offset(dims, values) : Nat}:
  %indices_of(dims, values, fits) : {Shape.row_major(dims, coordinate_of(dims, values, fits)) == Shape.offset(dims, _) : Nat}
  Equal.sym(Nat, Shape.offset(dims, Shape.indices(dims, coordinate_of(dims, values, fits))), Shape.row_major(dims, coordinate_of(dims, values, fits)), offset_indices(dims, coordinate_of(dims, values, 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=coordinate_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=indices_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=offset_indices
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=indices
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=offset
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=row_major