def copy_value_success

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as WordConversion
import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as Totality

1791def copy_value_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
1792  -source: Core.Tensor<input>, target: Core.Tensor<Layout.output(input, axes, plan)>, +value: F32,
1793  +inside: {True{} == U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))) : Bool}) ->
1794  Totality.CopySuccess<input, axes, plan, Transforms.copy_read(input, axes, plan, index,
1795    source => target => (source, Done{target}), target, (source, Done{value}))>:
1796  copy_written_success(input, axes, plan, Core.write_flat(Layout.output(input, axes, plan), target, index, value), source,
1797    {\{Totality.WriteSuccess: successful => successful} :
1798      Totality.WriteSuccess<Layout.output(input, axes, plan), target, index, value> ->
1799        {Totality.write_succeeded(Layout.output(input, axes, plan), Core.write_flat(Layout.output(input, axes, plan), target, index, value)) == True{} : Bool}}(
1800          tensor_write_success(Layout.output(input, axes, plan), target, index, value,
1801            Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))),
1802              %Shape.elements_exact(Layout.output(input, axes, plan)) :
1803                {True{} == Nat.is_lt(U32.to_nat(index), _) : Bool}
1804              %WordConversion.shape_count_exact(Layout.output(input, axes, plan)) :
1805                {True{} == Nat.is_lt(U32.to_nat(index), _) : Bool}
1806              %Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(Layout.output(input, axes, plan)))),
1807                U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))), Arith.u32_lt(index, Shape.count(Layout.output(input, axes, plan)))) :
1808                  {True{} == _ : Bool}
1809              inside))))