law lin_alphas_length

mlbend-generative@0.1.1.0 · main.bend:196

import Base

196# LAW 4 (lin_alphas_length): a linear schedule of t entries is t entries.
197law lin_alphas_length:
198  for +t: Nat
199  for +left: Nat
200  for +from: Nat
201  for +acc: F32
202  {List.length(&2, F32, lin_alphas_from(t, left, from, acc)) == left : Nat}