def success_keeps

bendtorch-core@0.1.0.0 · src/tensor/reduction_PROOF.bend:164

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/reduction_LAWS.bend as Laws

164def success_keeps(-shape: Shape.Shape, -original: Core.Tensor<shape>, -tensor: Core.Tensor<shape>,
165  result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>, +other: U32,
166  kept: {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}) ->
167  {Laws.successful_observe(shape, tensor, result, other) == Laws.successful_observe(shape, original, result, other) : Maybe<&2, F32>}:
168  match result:
169    case Fail{error}:
170      {==}
171    case Done{pair}:
172      kept