def offset_of

bendtorch-core@0.1.0.0 · src/shape/coordinate_proofs.bend:89

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

89def 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}:
90  %indices_of(dims, values, fits) : {Shape.row_major(dims, coordinate_of(dims, values, fits)) == Shape.offset(dims, _) : Nat}
91  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)))