law temb_length

mlbend-generative@0.1.1.0 · main.bend:247

import Base

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