law flatten_bounds_error

bendtorch-core@0.1.0.0 · src/shape/LAWS.bend:230

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

230# A coordinate of the shape's rank with a component outside its extent fails
231# with CoordinateOutOfBounds.
232law flatten_bounds_error:
233  for +shape: Shape.Shape
234  for +values: List<&2, U32>
235  for same: {Shape.rank_dimensions(Shape.dimensions(shape)) == Shape.rank_dimensions(values) : Nat}
236  for outside: {Shape.fit_words(Shape.dimensions(shape), values) == False{} : Bool}
237  {Shape.flatten_checked(shape, values) == Fail{Shape.CoordinateOutOfBounds{}} : Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>}