def somes_bumped

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

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

142def somes_bumped(slot: Maybe<&2, F32>, +rest: List<&2, Maybe<&2, F32>>, +below: Nat, +target: Nat, +value: F32, flag: Bool,
143  ih: {Laws.somes(Backward.bump(rest, below, target, value)) == Laws.mark(Laws.somes(rest), below, target) : List<&2, Bool>}) ->
144  {Laws.somes(Backward.bumped(slot, rest, value, unit => Backward.bump(rest, below, target, value), flag)) ==
145    Laws.marked(Maybe.is_some(&2, F32, slot), Laws.somes(rest), unit => Laws.mark(Laws.somes(rest), below, target), flag) : List<&2, Bool>}:
146  match flag:
147    case True{}:
148      Equal.cong(Bool, List<&2, Bool>, found => found <> Laws.somes(rest),
149        Maybe.is_some(&2, F32, Backward.accumulate(slot, Some{value})), True{}, is_some_accumulate(slot, value))
150    case False{}:
151      Equal.cong(List<&2, Bool>, List<&2, Bool>, xs => Maybe.is_some(&2, F32, slot) <> xs,
152        Laws.somes(Backward.bump(rest, below, target, value)), Laws.mark(Laws.somes(rest), below, target), ih)