def fit_indices

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

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

133def fit_indices(+dims: List<&2, Nat>, +coordinate: Shape.Coordinate(dims)) -> {True{} == Shape.fit(dims, Shape.indices(dims, coordinate)) : Bool}:
134  match dims:
135    case Nil{}:
136      match coordinate:
137        case Unit{}:
138          {==}
139    case +head <> +tail:
140      Shape.CStep{+index, +rest} = coordinate
141      %Nats.lt_true(Shape.Fin.value(head, index), head, Shape.Fin.bound(head, index)) : {True{} == Bool.and(_, Shape.fit(tail, Shape.indices(tail, rest))) : Bool}
142      fit_indices(tail, rest)