def accumulated_keeps

bendtorch-core@0.1.0.0 · src/autograd/gradient_PROOF.bend:784

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/autograd/gradient.bend as Gradient
import bendtorch-core@0.1.0.0/src/autograd/gradient_LAWS.bend as Laws

784def accumulated_keeps(-slot: Gradient.Slot, -contribution: Core.Dynamic, outcome: Gradient.Outcome,
785  -successful: {Laws.accumulated(outcome) == True{} : Bool}) -> Holds<Laws.RefusalKeeps(slot, contribution, outcome)>:
786  match outcome:
787    case Gradient.Accumulated{after}:
788      Holds{Unit{}}
789    case Gradient.Refused{after, returned, error}:
790      Holds{Empty.absurd(Laws.RefusalKeeps(slot, contribution, Gradient.Refused{after, returned, error}), Arith.clash(successful))}