GatherPROOF.Stepped: type of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend as GatherPROOF
Lines 445-452 of bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&start_line=445&end_line=452

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement

# One gradient cell of the backward: it skips, or adds its word.
type Stepped<-dg: Nat, -G: Array<F32>, -di: Nat, -I: Array<U32>, -i: Nat, -at: Nat, -slot: Nat, -acc: F32, -result: F32 & (Array<F32> & Array<U32>)> is Data:
  Skipped{-j: U32, -read: {Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(slot))) == Some{j} : Maybe<&2, U32>},
    -other: {Nat.is_eq(U32.to_nat(j), i) == False{} : Bool}, -kept: {result == (acc, (G, I)) : F32 & (Array<F32> & Array<U32>)}}
  Taken{-j: U32, -read: {Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(slot))) == Some{j} : Maybe<&2, U32>},
    -same: {Nat.is_eq(U32.to_nat(j), i) == True{} : Bool}, -x: F32,
    -word: {Model.observe(F32, dg, G, Refinement.route(dg, U32.from_nat(at))) == Some{x} : Maybe<&2, F32>},
    -kept: {result == (F32.add(acc, x), (G, I)) : F32 & (Array<F32> & Array<U32>)}}

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32.add
  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.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  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.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=route