def logical_observe_bridge

bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:2255

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

2255def logical_observe_bridge(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +index: U32,
2256  -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> ObserveBridge<shape, tensor, index>:
2257  ObserveBridge{
2258    {\{CheckedObservationModel: checked =>
2259      {\{ObserveBridge: equal => equal} : ObserveBridge<shape, tensor, index> ->
2260        {Core.checked_observe(shape, tensor, index) == Core.observe(shape, tensor, index) : Maybe<&2, F32>}}(
2261          observe_bridge(shape, tensor, index, checked))} : CheckedObservationModel<shape, tensor, index> ->
2262            {Core.checked_observe(shape, tensor, index) == Core.observe(shape, tensor, index) : Maybe<&2, F32>}}(
2263              checked_observation_model(shape, tensor, index, inside))}