ReductionPROOF.empty_values: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend as ReductionPROOF
Lines 375-389 of bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&start_line=375&end_line=389

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/reduction.bend as Reduction
import bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage

# A tensor with no storage holds no word.
def empty_values(-shape: Shape.Shape, -exact: {0n == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, fuel: Nat, +cursor: Nat,
  values: List<&2, F32>,
  logical: Laws.LogicalValues(fuel, shape, Core.TTensor{Storage.Empty{}, exact}, cursor, values)) ->
  Fact<{0.0 == Reduction.sequential_sum(values, 0.0) : F32}>:
  match fuel values:
    case 0n Nil{}:
      Fact{{==}}
    case 1n+rest +value <> others:
      Laws.LogicalStep{index_exact, observed, remaining} = logical
      Fact{Empty.absurd({0.0 == Reduction.sequential_sum(value <> others, 0.0) : F32}, no_value(value, observed))}
    case 0n value <> others:
      Empty.absurd(Fact<{0.0 == Reduction.sequential_sum(value <> others, 0.0) : F32}>, logical)
    case 1n+rest Nil{}:
      Empty.absurd(Fact<{0.0 == Reduction.sequential_sum(Nil{}, 0.0) : F32}>, logical)

Uses (14):
  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=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/storage/main.bend&name=Storage
  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/reduction.bend&name=sequential_sum
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend&name=LogicalStep
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend&name=LogicalValues
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&name=Fact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&name=no_value