def unflatten_checked
bendtorch-core@0.1.0.0 · src/shape/boundary_proofs.bend:179
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/LAWS.bend as Laws
179def unflatten_checked(+shape: Shape.Shape, +index: U32) -> {Laws.coordinate_result(shape, Shape.unflatten_checked(shape, index)) == Laws.unflatten_spec(Shape.extents(shape), Laws.fin_of(Shape.numel(Shape.extents(shape)), U32.to_nat(index))) : Maybe<&2, List<&2, U32>>}:
180 unflatten_verdict(shape, U32.to_nat(index), Shape.bool_case(Nat.is_lt(U32.to_nat(index), Shape.elements(shape))))