def checked_refusal
bendtorch-core@0.1.0.0 · src/autograd/gradient_PROOF.bend:833
import bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend as GradientPROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
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
833def checked_refusal(+shape: Shape.Shape, slot: Gradient.Slot, +contribution_shape: Shape.Shape, tensor: Core.Tensor<contribution_shape>, same: Bool,
834 -decided: {same == Layout.words_same(Shape.dimensions(contribution_shape), Shape.dimensions(shape)) : Bool}) ->
835 Holds<Laws.RefusalKeeps(slot, Core.Packed{contribution_shape, tensor}, Gradient.checked(shape, slot, contribution_shape, tensor, same))>:
836 match same:
837 case False{}:
838 Holds{({==}, (property => {==}, {\{Holds: proof => proof} : Holds<Laws.SlotKept(slot, slot)> -> Laws.SlotKept(slot, slot)}(slot_kept(slot))))}
839 case True{}:
840 agreed_refusal(shape, slot, Core.Packed{contribution_shape, tensor},
841 {\{Holds: proof => proof} : Holds<{Shape.dimensions(contribution_shape) == Shape.dimensions(shape) : List<&2, U32>}> ->
842 {Shape.dimensions(contribution_shape) == Shape.dimensions(shape) : List<&2, U32>}}(words_dimensions(contribution_shape, shape, decided)))