def unflatten_verdict
bendtorch-core@0.1.0.0 · src/shape/boundary_proofs.bend:165
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
165def unflatten_verdict(+shape: Shape.Shape, +index: Nat, +verdict: Shape.BoolCase<Nat.is_lt(index, Shape.elements(shape))>) -> {Laws.coordinate_result(shape, Shape.unflatten_checked.finish(shape, index, verdict)) == Laws.unflatten_spec(Shape.extents(shape), Laws.fin_of(Shape.numel(Shape.extents(shape)), index)) : Maybe<&2, List<&2, U32>>}:
166 match verdict:
167 case Shape.BFalse{equal}:
168 %fin_of_none(Shape.numel(Shape.extents(shape)), index, Coordinates.size_misses(shape, index, equal)) : {None{} == Laws.unflatten_spec(Shape.extents(shape), _) : Maybe<&2, List<&2, U32>>}
169 {==}
170 case Shape.BTrue{equal}:
171 +fits = Coordinates.size_fits(shape, index, equal)
172 +flat = Coordinates.fin_from(Shape.numel(Shape.extents(shape)), index, fits)
173 %Equal.sym(Maybe<&2, Shape.Fin(Shape.numel(Shape.extents(shape)))>, Laws.fin_of(Shape.numel(Shape.extents(shape)), index), Some{flat}, fin_of_from(Shape.numel(Shape.extents(shape)), index, fits)) : {Laws.coordinate_result(shape, Shape.coordinate_checked.nat(shape, Shape.digits_words(Shape.dimensions(shape), index))) == Laws.unflatten_spec(Shape.extents(shape), _) : Maybe<&2, List<&2, U32>>}
174 %Equal.sym(List<&2, Nat>, Shape.digits_words(Shape.dimensions(shape), index), Shape.digits(Shape.extents(shape), index), Coordinates.digits_words_spec(Shape.dimensions(shape), index)) : {Laws.coordinate_result(shape, Shape.coordinate_checked.nat(shape, _)) == Some{Shape.words(Shape.indices(Shape.extents(shape), Shape.unflatten(Shape.extents(shape), flat)))} : Maybe<&2, List<&2, U32>>}
175 %Coordinates.fin_from_value(Shape.numel(Shape.extents(shape)), index, fits) : {Laws.coordinate_result(shape, Shape.coordinate_checked.nat(shape, Shape.digits(Shape.extents(shape), _))) == Some{Shape.words(Shape.indices(Shape.extents(shape), Shape.unflatten(Shape.extents(shape), flat)))} : Maybe<&2, List<&2, U32>>}
176 %Coordinates.digits_unflatten(Shape.extents(shape), flat) : {Laws.coordinate_result(shape, Shape.coordinate_checked.nat(shape, _)) == Some{Shape.words(Shape.indices(Shape.extents(shape), Shape.unflatten(Shape.extents(shape), flat)))} : Maybe<&2, List<&2, U32>>}
177 checked_indices(shape, Shape.unflatten(Shape.extents(shape), flat))