type Stepped

bendtorch-core@0.1.0.0 · src/tensor/gather_PROOF.bend:445

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

445# One gradient cell of the backward: it skips, or adds its word.
446type 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:
447  Skipped{-j: U32, -read: {Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(slot))) == Some{j} : Maybe<&2, U32>},
448    -other: {Nat.is_eq(U32.to_nat(j), i) == False{} : Bool}, -kept: {result == (acc, (G, I)) : F32 & (Array<F32> & Array<U32>)}}
449  Taken{-j: U32, -read: {Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(slot))) == Some{j} : Maybe<&2, U32>},
450    -same: {Nat.is_eq(U32.to_nat(j), i) == True{} : Bool}, -x: F32,
451    -word: {Model.observe(F32, dg, G, Refinement.route(dg, U32.from_nat(at))) == Some{x} : Maybe<&2, F32>},
452    -kept: {result == (F32.add(acc, x), (G, I)) : F32 & (Array<F32> & Array<U32>)}}