MlbendGenerative.alphas_length: law of mlbend-generative@0.1.1.0
Import: import mlbend-generative@0.1.1.0/main.bend as MlbendGenerative
Lines 151-156 of mlbend-generative@0.1.1.0/main.bend: https://jend.leeeet.dev/read.txt?path=mlbend-generative@0.1.1.0/main.bend&start_line=151&end_line=156

import Base

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

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=mlbend-generative@0.1.1.0/main.bend&name=alphas_from