PermuteValues.cloned_lift: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/permute_values.bend as PermuteValues Lines 147-159 of bendtorch-core@0.1.0.0/src/tensor/permute_values.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&start_line=147&end_line=159 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/LAWS.bend as StorageLaws 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/layout.bend as Layout import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend as Owned import bendtorch-core@0.1.0.0/src/tensor/permute_build.bend as Build import bendtorch-core@0.1.0.0/src/storage/model.bend as Model import bendtorch-core@0.1.0.0/src/storage/api.bend as Api def cloned_lift(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +fill: F32, +ops: List<&2, StorageLaws.Op>, +d: Nat, -f: {Storage.bounds(d, U32.to_nat(Shape.count(Layout.output(input, axes, plan)))) == True{} : Bool}, -fo: {U32.to_nat(Shape.count(Layout.output(input, axes, plan))) == Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) : Nat}, +ds: Nat, -b: Model.Balanced(F32, ds, Api.arr(Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill)), -f2: {Storage.bounds(ds, U32.to_nat(Shape.count(input))) == True{} : Bool}, pair: Array & Array, -same: {pair == Array.clone(F32, Api.arr(Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill)) : Array & Array}, -sf: {Lifecycle.logical_length(Storage.Owned{ds, U32.to_nat(Shape.count(input)), Api.arr(Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill), b, f2}) == Shape.logical_numel(Shape.dimensions(input)) : Nat}, -Q: Core.Tensor & Result<&2, &1, Transforms.Error, Core.Dynamic> -> Type, hyp: @-kf: {Lifecycle.logical_length(StorageLaws.owner(Storage.Storage, Storage.finish_clone(ds, U32.to_nat(Shape.count(input)), Api.arr(Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill), pair, same, b, f2))) == Shape.logical_numel(Shape.dimensions(input)) : Nat} -> Packed(input, axes, plan, Q, StorageLaws.owner(Storage.Storage, Storage.finish_clone(ds, U32.to_nat(Shape.count(input)), Api.arr(Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill), pair, same, b, f2)), kf, Storage.Owned{d, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Build.build(d, Build.Request{input, axes}, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Pair.snd(Array, Array, pair)), Build.balanced(d, Build.Request{input, axes}, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Pair.snd(Array, Array, pair)), f}, fo)) -> Q(Transforms.copy_pack(input, axes, plan, Transforms.built_cloned(input, axes, plan, d, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), f, fo, ds, U32.to_nat(Shape.count(input)), Api.arr(Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill), pair, same, b, f2, sf))): (kept, copy) = pair hyp(sf) Uses (36): 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=F32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat 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=count 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/LAWS.bend&name=Op https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=owner https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=arr 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=finish_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/tensor/contracts/binary_storage_proof.bend&name=norm https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic 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/layout.bend&name=Plan https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=output https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=logical_length https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=Request https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=balanced https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=build https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=Packed https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=Error https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=built_cloned https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=copy_pack