GradientPROOF.finish_mapping: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend as GradientPROOF
Lines 505-537 of bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&start_line=505&end_line=537

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/transform_PROOF.bend as TransformProof
import bendtorch-core@0.1.0.0/src/autograd/gradient.bend as Gradient
import bendtorch-core@0.1.0.0/src/autograd/gradient_LAWS.bend as Laws

def finish_mapping(+total_shape: Shape.Shape, +shape: Shape.Shape, -total: Core.Tensor<total_shape>, -contribution: Core.Dynamic,
  outcome: Gradient.Outcome,
  -dimensions: {Shape.dimensions(total_shape) == Shape.dimensions(shape) : List<&2, U32>},
  -loop: LoopInv(total_shape, total, contribution, Nat.add(Shape.elements(total_shape), 0n), outcome)) ->
  Holds<Laws.Mapping(Gradient.Held{Core.Packed{total_shape, total}}, contribution, shape, outcome)>:
  match outcome:
    case Gradient.Refused{after, returned, error}:
      Holds{Unit{}}
    case Gradient.Accumulated{after}:
      Holds{(
        Equal.trans(Maybe<&2, List<&2, U32>>, Laws.held_dimensions(after), Some{Shape.dimensions(total_shape)}, Some{Shape.dimensions(shape)},
          Pair.fst(Dims(total_shape, after), Values(total_shape, total, contribution, Nat.add(Shape.elements(total_shape), 0n), after), loop),
          %dimensions : {Some{Shape.dimensions(total_shape)} == Some{_} : Maybe<&2, List<&2, U32>>}
          {==}),
        index => inside => Equal.trans(Maybe<&2, F32>, Laws.held_observe(after, index),
          partial(Nat.is_lt(U32.to_nat(index), Nat.add(Shape.elements(total_shape), 0n)),
            Core.checked_observe(total_shape, total, index), Core.checked_observe_dynamic(contribution, index)),
          Laws.add_word(Core.checked_observe(total_shape, total, index), Core.checked_observe_dynamic(contribution, index)),
          Pair.snd(Dims(total_shape, after), Values(total_shape, total, contribution, Nat.add(Shape.elements(total_shape), 0n), after), loop)(index)(
            %Equal.sym(List<&2, U32>, Shape.dimensions(total_shape), Shape.dimensions(shape), dimensions) :
              {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(_)) == True{} : Bool}
            inside),
          %Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), Nat.add(Shape.elements(total_shape), 0n)), True{},
            %Equal.sym(Nat, Nat.add(Shape.elements(total_shape), 0n), Shape.elements(total_shape), TransformProof.add_zero_right(Shape.elements(total_shape))) :
              {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
            %Equal.sym(Nat, Shape.elements(total_shape), Shape.numel(Shape.extents(total_shape)), Shape.elements_exact(total_shape)) :
              {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
            %Equal.sym(List<&2, U32>, Shape.dimensions(total_shape), Shape.dimensions(shape), dimensions) :
              {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(_)) == True{} : Bool}
            inside) :
            {partial(_, Core.checked_observe(total_shape, total, index), Core.checked_observe_dynamic(contribution, index)) ==
              Laws.add_word(Core.checked_observe(total_shape, total, index), Core.checked_observe_dynamic(contribution, index)) : Maybe<&2, F32>}
          {==}))}

Uses (38):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  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=Pair.fst
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd
  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=U32.to_nat
  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/gradient.bend&name=Outcome
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient.bend&name=Slot
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_LAWS.bend&name=Mapping
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_LAWS.bend&name=add_word
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_LAWS.bend&name=held_dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_LAWS.bend&name=held_observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=Dims
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=Holds
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=LoopInv
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=Values
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=partial
  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=elements
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=elements_exact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=extents
  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/core.bend&name=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
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=checked_observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=checked_observe_dynamic
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=add_zero_right