~/jendhub

def logical_original

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

import bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend as ReductionPROOF
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

512def logical_original(+fuel: Nat, -shape: Shape.Shape, -original: Core.Tensor<shape>, -tensor: Core.Tensor<shape>, +cursor: Nat,
513  values: List<&2, F32>, logical: Laws.LogicalValues(fuel, shape, tensor, cursor, values),
514  -kept: @+other: U32 -> {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}) ->
515  Laws.LogicalValues(fuel, shape, original, cursor, values):
516  logical_keeps(fuel, shape, tensor, original, cursor, values, logical,
517    other => Equal.sym(Maybe<&2, F32>, Core.checked_observe(shape, tensor, other), Core.checked_observe(shape, original, other), kept(other)))

Uses (11)

Used by (1)