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

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/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend as AllocationProof
import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as TransformTotality
import bendtorch-core@0.1.0.0/src/tensor/transform_LAWS.bend as TransformLaws

def fill_decided_success(+shape: Shape.Shape, +value: F32, +rest: List<&2, F32>, +cursor: Nat, +index: U32,
  decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>, -original: Core.Tensor<shape>,
  converted: {U32.to_nat(index) == cursor : Nat},
  -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
  -rec: @tensor: Core.Tensor<shape> -> FillSuccess<shape, Core.fill_values(rest, shape, tensor, 1n+cursor)>) ->
  FillSuccess<shape, 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}:
      FillSuccess{Empty.absurd({False{} == True{} : Bool}, Nats.contradiction(Nat.is_eq(U32.to_nat(index), cursor),
        AllocationProof.natural_equal_true(U32.to_nat(index), cursor, converted), equal))}
    case Shape.BTrue{equal}:
      FillSuccess{{\{FillSuccess: successful => successful} :
        FillSuccess<shape, Core.fill_values_step(shape, tensor => Core.fill_values(rest, shape, tensor, 1n+cursor),
          Core.write_flat(shape, original, index, value))> ->
        {Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>,
          Core.fill_values_step(shape, tensor => Core.fill_values(rest, shape, tensor, 1n+cursor),
            Core.write_flat(shape, original, index, value))) == True{} : Bool}}(
              fill_step_success(shape, rest, cursor, Core.write_flat(shape, original, index, value),
                {\{TransformTotality.WriteSuccess: successful => successful} : TransformTotality.WriteSuccess<shape, original, index, value> ->
                  {TransformTotality.write_succeeded(shape, Core.write_flat(shape, original, index, value)) == True{} : Bool}}(
                    TransformLaws.tensor_write_valid_success(shape, original, index, value, inside)), rec))}

Uses (27):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result.is_done
  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=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/shape/core.bend&name=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=contradiction
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend&name=natural_equal_true
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=FillSuccess
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=fill_step_success
  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=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/transform_LAWS.bend&name=tensor_write_valid_success
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend&name=WriteSuccess
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend&name=write_succeeded