def kept_observe

bendtorch-core@0.1.0.0 · src/tensor/matmul_PROOF.bend:1309

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/elementwise_totality.bend as ElementwiseTotality
import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as Parallel

1309def kept_observe(+shape: Shape.Shape, -a: Core.Tensor<shape>, -kept: Core.Tensor<shape>,
1310  -same: ElementwiseTotality.SameSource(Core.Packed{shape, a}, Core.Packed{shape, kept}), +other: U32) ->
1311  Parallel.Fact<{Core.checked_observe(shape, kept, other) == Core.checked_observe(shape, a, other) : Maybe<&2, F32>}>:
1312  Parallel.Fact{Equal.cong(ElementwiseTotality.Inspection, Maybe<&2, F32>, inspected,
1313    ElementwiseTotality.inspect(ElementwiseTotality.Checked{other}, Core.Packed{shape, kept}),
1314    ElementwiseTotality.inspect(ElementwiseTotality.Checked{other}, Core.Packed{shape, a}), same(ElementwiseTotality.Checked{other}))}