ReducePROOF.planned_zeros: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend as ReducePROOF
Lines 632-648 of bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&start_line=632&end_line=648

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as ShapeLaws
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce
import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as Laws

def planned_zeros(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape,
  result: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>,
  -sources: {ShapeLaws.planned_dimensions(target, shape, result) == (Shape.dimensions(target), Shape.dimensions(shape)) : List<&2, U32> & List<&2, U32>},
  -empty: {Shape.logical_numel(Shape.dimensions(shape)) == 0n : Nat}) ->
  Laws.Zeros<target, Reduce.planned(shape, tensor, target, result)>:
  match result:
    case Fail{error}:
      Laws.Zeros{Unit{}}
    case Done{+plan}:
      zeros_from_mapping(Core.Packed{shape, tensor}, target, plan, Reduce.planned(shape, tensor, target, Done{plan}),
        {\{Holds: proof => proof} :
          Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan}, Reduce.planned(shape, tensor, target, Done{plan}))> ->
          Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan}, Reduce.planned(shape, tensor, target, Done{plan}))}(
          planned_mapping(shape, tensor, target, Done{plan}, sources)),
        {\{Holds: proof => proof} : Holds<Laws.Listed(Core.Packed{shape, tensor}, Nil{})> -> Laws.Listed(Core.Packed{shape, tensor}, Nil{})}(
          listed_empty(Core.Packed{shape, tensor}, empty)),
        empty)

Uses (23):
  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=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=U32
  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/autograd/reduce.bend&name=planned
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend&name=Listed
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend&name=MappingWith
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend&name=Zeros
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&name=Holds
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&name=listed_empty
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&name=planned_mapping
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&name=zeros_from_mapping
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=planned_dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BroadcastPlan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Error
  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/tensor/core.bend&name=Dynamic
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor