def flatten_row_major

bendtorch-core@0.1.0.0 · src/shape/index_proofs.bend:147

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

147def flatten_row_major(+dims: List<&2, Nat>, +coordinate: Shape.Coordinate(dims)) -> {Shape.Fin.value(Shape.numel(dims), Shape.flatten(dims, coordinate)) == Shape.row_major(dims, coordinate) : Nat}:
148  match dims:
149    case Nil{}:
150      {==}
151    case +head <> +tail:
152      Shape.CStep{+first, +rest} = coordinate
153      %flatten_row_major(tail, rest) : {Shape.Fin.value(Shape.numel(head <> tail), Shape.flatten(head <> tail, Shape.CStep{first, rest})) == Nat.add(Nat.mul(Shape.Fin.value(head, first), Shape.numel(tail)), _) : Nat}
154      pack_value(head, Shape.numel(tail), first, Shape.flatten(tail, rest))