def checked_indices
bendtorch-core@0.1.0.0 · src/shape/boundary_proofs.bend:121
import bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend as BoundaryProofs
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates
import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as Laws
121def checked_indices(+shape: Shape.Shape, +coordinate: Shape.Coordinate(Shape.extents(shape))) -> {Laws.coordinate_result(shape, Shape.coordinate_checked.nat(shape, Shape.indices(Shape.extents(shape), coordinate))) == Some{Shape.words(Shape.indices(Shape.extents(shape), coordinate))} : Maybe<&2, List<&2, U32>>}:
122 +values = Shape.indices(Shape.extents(shape), coordinate)
123 checked_fit(shape, values, Shape.bool_case(Shape.fit_values(Shape.dimensions(shape), values)), Coordinates.fit_indices(Shape.extents(shape), coordinate))