law arrays_len

bend-ml-llama@0.2.1.0 · main.bend:511

import Base

511# LAW (arrays_len): arrays(n, d) makes exactly n arrays.
512law arrays_len:
513  for +n: Nat
514  for +d: Nat
515  {List.length(&1, Array<F32>, arrays(n, d)) == n : Nat}