Frame.primitive_frame_cloned: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/storage/frame.bend as Frame
Lines 77-92 of bendtorch-core@0.1.0.0/src/storage/frame.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/storage/frame.bend&start_line=77&end_line=92

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

def primitive_frame_cloned(-T: Data, +d: Nat, -original: Array<T>, +i: U32,
  +other: Model.Path(d), +value: T, cloned: Clone.Cloned<T, d, original>) ->
  {Model.observe(T, d, Array.set(T, original, i, value), other) == Model.select(T, Model.same(d, Refinement.route(d, i), other), value, Model.observe(T, d, original, other)) : Maybe<&2, T>}:
  match cloned:
    case Clone.Cloned{first, second, exact, +same_first, +same_second, valid_first, valid_second}:
      %same_second :
        {Model.observe(T, d, Array.set(T, original, i, value), other) == Model.select(T, Model.same(d, Refinement.route(d, i), other), value, Model.observe(T, d, _, other)) : Maybe<&2, T>}
      %same_first :
        {Model.observe(T, d, Array.set(T, _, i, value), other) == Model.select(T, Model.same(d, Refinement.route(d, i), other), value, Model.observe(T, d, second, other)) : Maybe<&2, T>}
      %Equal.sym(Array<T>, Array.set(T, first, i, value), ArrayCore.write_path(T, d, first, Refinement.route(d, i), value),
        Refinement.law_set_refines(T, d, first, i, value, valid_first)) :
        {Model.observe(T, d, _, other) == Model.select(T, Model.same(d, Refinement.route(d, i), other), value, Model.observe(T, d, second, other)) : Maybe<&2, T>}
      %Equal.trans(Array<T>, second, original, first, same_second,
        Equal.sym(Array<T>, first, original, same_first)) :
        {Model.observe(T, d, ArrayCore.write_path(T, d, _, Refinement.route(d, i), value), other) == Model.select(T, Model.same(d, Refinement.route(d, i), other), value, Model.observe(T, d, second, other)) : Maybe<&2, T>}
      update_frame(T, d, second, Refinement.route(d, i), other, value, valid_second)

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.set
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/array.bend&name=write_path
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/clone.bend&name=Cloned
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/frame.bend&name=update_frame
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Path
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=same
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=select
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=law_set_refines
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=route