law alphas_length

mlbend-generative@0.1.1.0 · main.bend:151

import Base

151# LAW 2 (alphas_length): a schedule of t entries is t entries.
152law alphas_length:
153  for +t: Nat
154  for +left: Nat
155  for +from: Nat
156  {List.length(&2, F32, alphas_from(t, left, from)) == left : Nat}