MlbendGenerative.temb_length: law of mlbend-generative@0.1.1.0
Import: import mlbend-generative@0.1.1.0/main.bend as MlbendGenerative
Lines 247-253 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=247&end_line=253

import Base

# LAW 3 (temb_length): an embedding of k rungs is 2k numbers.
law temb_length:
  for +t: Nat
  for +steps: Nat
  for +k: Nat
  for +p: Nat
  {List.length(&2, F32, temb_from(t, steps, k, p)) == Nat.mul(k, 2n) : Nat}

Uses (6):
  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=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=mlbend-generative@0.1.1.0/main.bend&name=temb_from