~/jendhub

def output_inside

bendtorch-core@0.1.0.0 · src/tensor/elementwise_parallel_proof.bend:451

import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as ElementwiseParallelProof
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats

451def output_inside(+plan: Shape.BroadcastPlan, +length: Nat, +index: U32,
452  +exact: {length == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat},
453  +bound: Shape.LT(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))))) -> {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}:
454  %Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
455  Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))), Nats.lt_true(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), bound))

Uses (12)

Used by (1)