BatchedMatmulLAWS.batched_build_balanced: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend as BatchedMatmulLAWS
Lines 161-171 of bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend&start_line=161&end_line=171

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend as Batched

# The build is a balanced tree of its depth, whatever the split: the
# certificate the output storage carries.
law batched_build_balanced:
  for +depth: Nat
  for +splits: Nat
  for +given: Batched.Layout
  for +count: Nat
  for +base: Nat
  for la: Array<F32>
  for ra: Array<F32>
  Model.Balanced(F32, depth, Batched.build(depth, splits, given, count, base, la, ra))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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/batched_matmul.bend&name=Layout
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&name=build
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&name=build_balanced