law copy_write_frame

bendtorch-core@0.1.0.0 · src/tensor/transform_LAWS.bend:99

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement

99law copy_write_frame:
100  for +depth: Nat
101  for array: Array<F32>
102  for +index: U32
103  for +other: U32
104  for +value: F32
105  for balanced: Model.Balanced(F32, depth, array)
106  {Model.observe(F32, depth, Array.set(F32, array, index, value), Refinement.route(depth, other)) ==
107    Model.select(F32, Model.same(depth, Refinement.route(depth, index), Refinement.route(depth, other)), value,
108      Model.observe(F32, depth, array, Refinement.route(depth, other))) : Maybe<&2, F32>}