ConstructionPROOF.clone_owned_meaning: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend as ConstructionPROOF Lines 88-144 of bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&start_line=88&end_line=144 import Base import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage 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 import bendtorch-core@0.1.0.0/src/storage/clone.bend as Clone import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle import bendtorch-core@0.1.0.0/src/tensor/construction_LAWS.bend as Laws def clone_owned_meaning(-shape: Shape.Shape, +depth: Nat, +length: Nat, -array: Array, -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool}, -length_exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) -> Laws.CloneMeaning: Laws.CloneMeaning{ index => Equal.trans(Maybe<&2, F32>, Laws.clone_first_checked(shape, Core.clone(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, length_exact}), index), Lifecycle.checked_observe(Pair.fst(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index), Lifecycle.checked_observe_array(depth, length, array, index), clone_first_checked_view(shape, Storage.Owned{depth, length, array, balanced, valid}, length_exact, index, Storage.clone(Storage.Owned{depth, length, array, balanced, valid}), {==}), Equal.trans(Maybe<&2, F32>, Lifecycle.checked_observe(Pair.fst(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index), Lifecycle.checked_observe_array(depth, length, Pair.fst(Array, Array, Array.clone(F32, array)), index), Lifecycle.checked_observe_array(depth, length, array, index), storage_clone_first_checked_view(depth, length, array, index, Array.clone(F32, array), {==}, balanced, valid), Equal.cong(Array, Maybe<&2, F32>, a => Lifecycle.checked_observe_array(depth, length, a, index), Pair.fst(Array, Array, Array.clone(F32, array)), array, Clone.first_equal(F32, depth, array, Clone.certify(F32, depth, array, balanced))))), index => Equal.trans(Maybe<&2, F32>, Laws.clone_second_checked(shape, Core.clone(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, length_exact}), index), Lifecycle.checked_observe(Pair.snd(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index), Lifecycle.checked_observe_array(depth, length, array, index), clone_second_checked_view(shape, Storage.Owned{depth, length, array, balanced, valid}, length_exact, index, Storage.clone(Storage.Owned{depth, length, array, balanced, valid}), {==}), Equal.trans(Maybe<&2, F32>, Lifecycle.checked_observe(Pair.snd(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index), Lifecycle.checked_observe_array(depth, length, Pair.snd(Array, Array, Array.clone(F32, array)), index), Lifecycle.checked_observe_array(depth, length, array, index), storage_clone_second_checked_view(depth, length, array, index, Array.clone(F32, array), {==}, balanced, valid), Equal.cong(Array, Maybe<&2, F32>, a => Lifecycle.checked_observe_array(depth, length, a, index), Pair.snd(Array, Array, Array.clone(F32, array)), array, Clone.second_equal(F32, depth, array, Clone.certify(F32, depth, array, balanced))))), index => Equal.trans(Maybe<&2, F32>, Laws.clone_first_model(shape, Core.clone(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, length_exact}), index), Lifecycle.observe(Pair.fst(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index), Model.observe(F32, depth, array, Refinement.route(depth, index)), clone_first_model_view(shape, Storage.Owned{depth, length, array, balanced, valid}, length_exact, index, Storage.clone(Storage.Owned{depth, length, array, balanced, valid}), {==}), Equal.trans(Maybe<&2, F32>, Lifecycle.observe(Pair.fst(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index), Model.observe(F32, depth, Pair.fst(Array, Array, Array.clone(F32, array)), Refinement.route(depth, index)), Model.observe(F32, depth, array, Refinement.route(depth, index)), storage_clone_first_model_view(depth, length, array, index, Array.clone(F32, array), {==}, balanced, valid), Equal.cong(Array, Maybe<&2, F32>, a => Model.observe(F32, depth, a, Refinement.route(depth, index)), Pair.fst(Array, Array, Array.clone(F32, array)), array, Clone.first_equal(F32, depth, array, Clone.certify(F32, depth, array, balanced))))), index => Equal.trans(Maybe<&2, F32>, Laws.clone_second_model(shape, Core.clone(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, length_exact}), index), Lifecycle.observe(Pair.snd(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index), Model.observe(F32, depth, array, Refinement.route(depth, index)), clone_second_model_view(shape, Storage.Owned{depth, length, array, balanced, valid}, length_exact, index, Storage.clone(Storage.Owned{depth, length, array, balanced, valid}), {==}), Equal.trans(Maybe<&2, F32>, Lifecycle.observe(Pair.snd(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index), Model.observe(F32, depth, Pair.snd(Array, Array, Array.clone(F32, array)), Refinement.route(depth, index)), Model.observe(F32, depth, array, Refinement.route(depth, index)), storage_clone_second_model_view(depth, length, array, index, Array.clone(F32, array), {==}, balanced, valid), Equal.cong(Array, Maybe<&2, F32>, a => Model.observe(F32, depth, a, Refinement.route(depth, index)), Pair.snd(Array, Array, Array.clone(F32, array)), array, Clone.second_equal(F32, depth, array, Clone.certify(F32, depth, array, balanced)))))} Uses (40): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.clone https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 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=Pair.fst https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/clone.bend&name=certify https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/clone.bend&name=first_equal https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/clone.bend&name=second_equal https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=Storage https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=bounds https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=clone https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Balanced 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/refinement.bend&name=route https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_LAWS.bend&name=CloneMeaning https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_LAWS.bend&name=clone_first_checked https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_LAWS.bend&name=clone_first_model https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_LAWS.bend&name=clone_second_checked https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_LAWS.bend&name=clone_second_model https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=clone_first_checked_view https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=clone_first_model_view https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=clone_second_checked_view https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=clone_second_model_view https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=storage_clone_first_checked_view https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=storage_clone_first_model_view https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=storage_clone_second_checked_view https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=storage_clone_second_model_view https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=clone https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=checked_observe https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=checked_observe_array https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=observe