def observe_bridge

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

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/storage/main.bend as Storage

393def observe_bridge(-shape: Shape.Shape, tensor: Core.Tensor<shape>, +index: U32,
394  checked: Core.ObservationChecked(Core.Packed{shape, tensor}, index)) -> ObserveBridge<shape, tensor, index>:
395  Core.TTensor{storage, exact} = tensor
396  match storage:
397    case Storage.Empty{}:
398      ObserveBridge{{==}}
399    case Storage.Owned{+depth, +length, array, balanced, valid}:
400      ObserveBridge{observe_allowed_equal(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length),
401        route_allowed(depth, length, index, checked), checked)}