BoundaryProofs.flatten_fits: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend as BoundaryProofs
Lines 141-152 of bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&start_line=141&end_line=152

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

def flatten_fits(+shape: Shape.Shape, +values: List<&2, U32>, +verdict: Shape.BoolCase<Shape.fit_words(Shape.dimensions(shape), values)>) -> {Laws.index_result(shape, Shape.flatten_checked.fits(shape, values, verdict)) == Laws.flatten_spec(Shape.extents(shape), Laws.decode(Shape.extents(shape), Shape.naturals(values))) : Maybe<&2, U32>}:
  match verdict:
    case Shape.BFalse{equal}:
      %decode_unfit(Shape.extents(shape), Shape.naturals(values), fit_words_false(Shape.dimensions(shape), values, equal)) : {None{} == Laws.flatten_spec(Shape.extents(shape), _) : Maybe<&2, U32>}
      {==}
    case Shape.BTrue{equal}:
      +fits = Coordinates.fits_of(Shape.extents(shape), Shape.naturals(values), fit_words_true(Shape.dimensions(shape), values, equal))
      +coordinate = Coordinates.coordinate_of(Shape.extents(shape), Shape.naturals(values), fits)
      +flat = Shape.horner(Shape.dimensions(shape), values, 0n)
      %Equal.sym(Maybe<&2, Shape.Coordinate(Shape.extents(shape))>, Laws.decode(Shape.extents(shape), Shape.naturals(values)), Some{coordinate}, decode_fit(Shape.extents(shape), Shape.naturals(values), fits)) : {Laws.index_result(shape, Shape.flat_checked(shape, flat)) == Laws.flatten_spec(Shape.extents(shape), _) : Maybe<&2, U32>}
      %horner_fits(shape, values, fits) : {Laws.index_result(shape, Shape.flat_checked(shape, flat)) == Some{U32.from_nat(_)} : Maybe<&2, U32>}
      flat_view(shape, flat, Shape.bool_case(Nat.is_lt(flat, Shape.elements(shape))), horner_below(shape, values, fits))

Uses (30):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=decode
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=flatten_spec
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=index_result
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=decode_fit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=decode_unfit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=fit_words_false
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=fit_words_true
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=flat_view
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=horner_below
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=horner_fits
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=coordinate_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=fits_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BoolCase
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Coordinate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=bool_case
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=elements
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=extents
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=fit_words
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=flat_checked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=flatten_checked.fits
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=horner
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=naturals