def expected_left_same

bendtorch-core@0.1.0.0 · src/tensor/core_PROOF.bend:711

import Base
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise

711def expected_left_same(+operation: Elementwise.Operation, -current: Core.Dynamic, -original: Core.Dynamic, +index: U32,
712  left: Maybe<&2, F32>, equal: {Core.checked_observe_dynamic(current, index) == Core.checked_observe_dynamic(original, index) : Maybe<&2, F32>}) ->
713  {Elementwise.expected_left(operation, current, index, left) == Elementwise.expected_left(operation, original, index, left) : Maybe<&2, F32>}:
714  match left:
715    case None{}:
716      {==}
717    case Some{+value}:
718      Equal.cong(Maybe<&2, F32>, Maybe<&2, F32>, right => Elementwise.expected_right(operation, value, right),
719        Core.checked_observe_dynamic(current, index), Core.checked_observe_dynamic(original, index), equal)