def somes_bump

bendtorch-core@0.1.0.0 · src/autograd/backward_PROOF.bend:154

import Base
import bendtorch-core@0.1.0.0/src/autograd/backward.bend as Backward
import bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend as Laws

154def somes_bump(slots: List<&2, Maybe<&2, F32>>, +count: Nat, +target: Nat, +value: F32) ->
155  {Laws.somes(Backward.bump(slots, count, target, value)) == Laws.mark(Laws.somes(slots), count, target) : List<&2, Bool>}:
156  match slots count:
157    case Nil{} count:
158      {==}
159    case Con{slot, rest} 0n:
160      {==}
161    case Con{slot, +rest} 1n+below:
162      somes_bumped(slot, rest, below, target, value, Nat.is_eq(below, target), somes_bump(rest, below, target, value))