def flatten_ranked
bendtorch-core@0.1.0.0 · src/shape/boundary_proofs.bend:154
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
154def flatten_ranked(+shape: Shape.Shape, +values: List<&2, U32>, +same: Shape.BoolCase<Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.rank_dimensions(values))>) -> {Laws.index_result(shape, Shape.flatten_checked.ranked(shape, values, same)) == Laws.flatten_spec(Shape.extents(shape), Laws.decode(Shape.extents(shape), Shape.naturals(values))) : Maybe<&2, U32>}:
155 match same:
156 case Shape.BFalse{equal}:
157 %decode_rank(Shape.dimensions(shape), values, equal) : {None{} == Laws.flatten_spec(Shape.extents(shape), _) : Maybe<&2, U32>}
158 {==}
159 case Shape.BTrue{equal}:
160 flatten_fits(shape, values, Shape.bool_case(Shape.fit_words(Shape.dimensions(shape), values)))