def offset_indices

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

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

69def offset_indices(+dims: List<&2, Nat>, +coordinate: Shape.Coordinate(dims)) -> {Shape.offset(dims, Shape.indices(dims, coordinate)) == Shape.row_major(dims, coordinate) : Nat}:
70  match dims:
71    case Nil{}:
72      {==}
73    case +head <> +tail:
74      Shape.CStep{+index, +rest} = coordinate
75      Equal.cong(Nat, Nat, value => Nat.add(Nat.mul(Shape.Fin.value(head, index), Shape.numel(tail)), value), Shape.offset(tail, Shape.indices(tail, rest)), Shape.row_major(tail, rest), offset_indices(tail, rest))