ConstructionPROOF.fill_advance: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend as ConstructionPROOF
Lines 278-305 of bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&start_line=278&end_line=305

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/construction_LAWS.bend as Laws

def fill_advance(-shape: Shape.Shape, +value: F32, +rest: List<&2, F32>, +cursor: Nat,
  -original: Core.Tensor<shape>, -written: Core.Tensor<shape>,
  result: Result<&2, &1, Core.Error, Core.Tensor<shape>>, -point: Written<shape, original, written, cursor, value>,
  -next: FillMeaning(shape, written, rest, 1n+cursor, result)) -> FillOutcome<shape, original, value <> rest, cursor, result>:
  match result:
    case Fail{error}:
      FillOutcome{Unit{}}
    case Done{tensor}:
      FillOutcome{
        (index => offset => at => inside =>
          {\{Written: observed => before =>
            {\{Tuple: mapping => after => fill_elements_advance(shape, value, rest, cursor, written, tensor,
              observed, mapping, after, index, offset, at, inside)} :
              (FillElements(shape, rest, 1n+cursor, tensor) & FillFrame(shape, written, 1n+cursor, tensor)) ->
                (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
                  {Core.checked_observe(shape, tensor, index) == Laws.list_element(value <> rest, offset) : Maybe<&2, F32>})}(next)
          } : Written<shape, original, written, cursor, value> ->
            (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
              {Core.checked_observe(shape, tensor, index) == Laws.list_element(value <> rest, offset) : Maybe<&2, F32>})}(point),
          index => earlier => checked =>
            {\{Written: observed => before =>
              {\{Tuple: mapping => after => fill_frame_advance(shape, original, written, tensor, cursor, before, after, index, earlier, checked)} :
                (FillElements(shape, rest, 1n+cursor, tensor) & FillFrame(shape, written, 1n+cursor, tensor)) ->
                  (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
                    {Core.checked_observe(shape, tensor, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>})}(next)
            } : Written<shape, original, written, cursor, value> ->
              (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
                {Core.checked_observe(shape, tensor, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>})}(point))}

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  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
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  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/tensor/construction_LAWS.bend&name=list_element
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=FillElements
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=FillFrame
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=FillMeaning
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=FillOutcome
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=Written
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=fill_elements_advance
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=fill_frame_advance
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=ObservationChecked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=checked_observe