def indices_of

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

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

55def 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>}:
56  match dims values:
57    case Nil{} Nil{}:
58      {==}
59    case +dh <> +dt +vh <> +vt:
60      FStep{+bound, +tail} = fits
61      %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>}
62      %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>}
63      {==}
64    case Nil{} vh <> vt:
65      match fits:
66    case dh <> dt Nil{}:
67      match fits: