PermuteBuildProof.build_cell: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend as PermuteBuildProof Lines 301-320 of bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&start_line=301&end_line=320 import Base import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape 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/tensor/parallel_proofs.bend as Generic # Every slot of the build holds what its cell function computes. def build_cell(+depth: Nat, +input: Shape.Shape, +axes: List<&2, U32>, +count: Nat, +d: Nat, -a: Array, +path: Model.Path(depth), -valid: Model.Balanced(F32, d, a)) -> Fact<{Model.observe(F32, depth, Build.build(depth, Build.Request{input, axes}, count, a), path) == Some{Pair.fst(F32, Array & Array, Build.cell(Build.recipe(Build.Request{input, axes}), Nat.add(Model.offset(depth, path), 0n), (a, Array.new(F32, 0n, 0.0)), Nat.is_lt(Nat.add(Model.offset(depth, path), 0n), count)))} : Maybe<&2, F32>}>: +request : Build.Request = Build.Request{input, axes} Fact{{\{Generic.Fact: q => q} : Generic.Fact, ~Array, ~Build.cell, Build.recipe(request), (a, Array.new(F32, 0n, 0.0)), depth, count, 0n, Build.build(depth, request, count, a))> -> Generic.Cells(~Build.Recipe, ~Array, ~Array, ~Build.cell, Build.recipe(request), (a, Array.new(F32, 0n, 0.0)), depth, count, 0n, Build.build(depth, request, count, a))}( Generic.build_cells(~Build.Request, ~Build.Recipe, ~Array, ~Array, ~Build.recipe, ~Build.split, ~Build.cell, request, (a, Array.new(F32, 0n, 0.0)), depth, Build.splits(depth), count, 0n, (a, Array.new(F32, 0n, 0.0)), {==}, at => inside => {\{Fact: q => q} : Fact<{Pair.snd(F32, Array & Array, Build.cell(Build.recipe(request), at, (a, Array.new(F32, 0n, 0.0)), inside)) == (a, Array.new(F32, 0n, 0.0)) : Array & Array}> -> {Pair.snd(F32, Array & Array, Build.cell(Build.recipe(request), at, (a, Array.new(F32, 0n, 0.0)), inside)) == (a, Array.new(F32, 0n, 0.0)) : Array & Array}}(cell_keeps(d, a, request, at, inside, valid)), Pair.fst({Pair.fst(Array & Array, Array & Array, Build.split((a, Array.new(F32, 0n, 0.0)))) == (a, Array.new(F32, 0n, 0.0)) : Array & Array}, {Pair.snd(Array & Array, Array & Array, Build.split((a, Array.new(F32, 0n, 0.0)))) == (a, Array.new(F32, 0n, 0.0)) : Array & Array}, {\{Fact: q => q} : Fact -> SplitFacts(a)}(split_equal(d, a, valid))), Pair.snd({Pair.fst(Array & Array, Array & Array, Build.split((a, Array.new(F32, 0n, 0.0)))) == (a, Array.new(F32, 0n, 0.0)) : Array & Array}, {Pair.snd(Array & Array, Array & Array, Build.split((a, Array.new(F32, 0n, 0.0)))) == (a, Array.new(F32, 0n, 0.0)) : Array & Array}, {\{Fact: q => q} : Fact -> SplitFacts(a)}(split_equal(d, a, valid)))))(path)} Uses (32): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.new 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=Maybe https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair 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=Base/base.bend&name=Sigma 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/shape/core.bend&name=Shape 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=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=offset https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Cells https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Fact https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=build_cells https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=Recipe 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=build https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=cell https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=recipe https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=split https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=splits https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=Fact https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=SplitFacts https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=cell_keeps https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=split_equal