GatherLAWS.AddStep: type of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend as GatherLAWS
Lines 286-297 of bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend&start_line=286&end_line=297

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
import bendtorch-core@0.1.0.0/src/tensor/gather.bend as Gather

type AddStep<-dg: Nat, -G: Array<F32>, -di: Nat, -I: Array<U32>, -kind: Gather.Lookup, -count: Nat, -inner: Nat, -o: Nat, -i: Nat, -r: Nat,
  -rest: Nat, -k: Nat, -acc: F32, -value: F32> is Data:
  Skips{-j: U32,
    -read: {Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(entry_at(kind, count, inner, o, k, r)))) == Some{j} : Maybe<&2, U32>},
    -other: {Nat.is_eq(U32.to_nat(j), i) == False{} : Bool},
    -next: Added(dg, G, di, I, kind, count, inner, o, i, r, rest, 1n+k, acc, value)}
  Adds{-j: U32,
    -read: {Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(entry_at(kind, count, inner, o, k, r)))) == 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(position(count, inner, o, k, r)))) == Some{x} : Maybe<&2, F32>},
    -next: Added(dg, G, di, I, kind, count, inner, o, i, r, rest, 1n+k, F32.add(acc, x), value)}

Uses (16):
  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=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
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=Lookup
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend&name=Added
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend&name=entry_at
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend&name=position