ConstructionPROOF.fill_decision_model: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend as ConstructionPROOF
Lines 460-475 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=460&end_line=475

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/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CoreProof

def fill_decision_model(-shape: Shape.Shape, +value: F32, +rest: List<&2, F32>, +cursor: Nat, +index: U32,
  -original: Core.Tensor<shape>, decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>,
  -rec: @tensor: Core.Tensor<shape> -> FillOutcome<shape, tensor, rest, 1n+cursor, Core.fill_values(rest, shape, tensor, 1n+cursor)>) ->
  FillOutcome<shape, original, value <> rest, cursor, Core.fill_values_decided(shape, cursor, index, value, original,
    tensor => Core.fill_values(rest, shape, tensor, 1n+cursor), decision)>:
  match decision:
    case Shape.BFalse{equal}:
      FillOutcome{Unit{}}
    case Shape.BTrue{equal}:
      FillOutcome{
        {\{FillOutcome: meaning => meaning} :
          FillOutcome<shape, original, value <> rest, cursor,
            Core.fill_values_step(shape, tensor => Core.fill_values(rest, shape, tensor, 1n+cursor), Core.write_flat(shape, original, index, value))> ->
          FillMeaning(shape, original, value <> rest, cursor,
            Core.fill_values_step(shape, tensor => Core.fill_values(rest, shape, tensor, 1n+cursor), Core.write_flat(shape, original, index, value)))}(fill_write_pair(shape, value, rest, cursor, index, original, Core.write_flat(shape, original, index, value), {==},
                Lifecycle.natural_equal(U32.to_nat(index), cursor, equal), CoreProof.checked_update_model(shape, original, index, value), rec))}

Uses (19):
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  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=BoolCase
  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_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=fill_write_pair
  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=fill_values
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=fill_values_decided
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=fill_values_step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=write_flat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=checked_update_model
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=natural_equal