def indices_length

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

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

89def indices_length(+dims: List<&2, Nat>, +coordinate: Shape.Coordinate(dims)) -> {List.length(&2, Nat, dims) == List.length(&2, Nat, Shape.indices(dims, coordinate)) : Nat}:
90  match dims:
91    case Nil{}:
92      {==}
93    case +head <> +tail:
94      Shape.CStep{+index, +rest} = coordinate
95      %indices_length(tail, rest) : {1n+List.length(&2, Nat, tail) == 1n+_ : Nat}
96      {==}