def planned_zeros
bendtorch-core@0.1.0.0 · src/autograd/reduce_PROOF.bend:632
import bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend as ReducePROOF
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
632def planned_zeros(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape,
633 result: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>,
634 -sources: {ShapeLaws.planned_dimensions(target, shape, result) == (Shape.dimensions(target), Shape.dimensions(shape)) : List<&2, U32> & List<&2, U32>},
635 -empty: {Shape.logical_numel(Shape.dimensions(shape)) == 0n : Nat}) ->
636 Laws.Zeros<target, Reduce.planned(shape, tensor, target, result)>:
637 match result:
638 case Fail{error}:
639 Laws.Zeros{Unit{}}
640 case Done{+plan}:
641 zeros_from_mapping(Core.Packed{shape, tensor}, target, plan, Reduce.planned(shape, tensor, target, Done{plan}),
642 {\{Holds: proof => proof} :
643 Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan}, Reduce.planned(shape, tensor, target, Done{plan}))> ->
644 Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan}, Reduce.planned(shape, tensor, target, Done{plan}))}(
645 planned_mapping(shape, tensor, target, Done{plan}, sources)),
646 {\{Holds: proof => proof} : Holds<Laws.Listed(Core.Packed{shape, tensor}, Nil{})> -> Laws.Listed(Core.Packed{shape, tensor}, Nil{})}(
647 listed_empty(Core.Packed{shape, tensor}, empty)),
648 empty)