law batched_build_balanced

bendtorch-core@0.1.0.0 · src/tensor/batched_matmul_LAWS.bend:161

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

161# The build is a balanced tree of its depth, whatever the split: the
162# certificate the output storage carries.
163law batched_build_balanced:
164  for +depth: Nat
165  for +splits: Nat
166  for +given: Batched.Layout
167  for +count: Nat
168  for +base: Nat
169  for la: Array<F32>
170  for ra: Array<F32>
171  Model.Balanced(F32, depth, Batched.build(depth, splits, given, count, base, la, ra))