def contribution_room
bendtorch-core@0.1.0.0 · src/autograd/reduce_fold_PROOF.bend:205
import bendtorch-core@0.1.0.0/src/autograd/reduce_fold_PROOF.bend as ReduceFoldPROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
205def contribution_room(+plan: Shape.BroadcastPlan,
206 same: {Shape.extents(Shape.output_shape(plan)) == Shape.extents(Shape.right_shape(plan)) : List<&2, Nat>}) ->
207 {Nat.is_le(Shape.elements(Shape.right_shape(plan)), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) == True{} : Bool}:
208 +right = Shape.right_shape(plan)
209 +limit = Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))
210 %Equal.sym(Nat, Shape.elements(right), Shape.numel(Shape.extents(right)), Shape.elements_exact(right)) :
211 {Nat.is_le(_, limit) == True{} : Bool}
212 %Equal.cong(List<&2, Nat>, Nat, extents => Shape.numel(extents), Shape.extents(Shape.output_shape(plan)), Shape.extents(right), same) :
213 {Nat.is_le(_, limit) == True{} : Bool}
214 Conversion.le_reflexive(limit)