law ddim_length

mlbend-generative@0.1.1.0 · main.bend:406

import Base

406# LAW 6 (ddim_length): a step over n elements is n elements.
407law ddim_length:
408  for +co: Step
409  for +x: List<&2, F32>
410  for +eps: List<&2, F32>
411  for +z: List<&2, F32>
412  {List.length(&2, F32, ddim(co, x, eps, z)) == List.length(&2, F32, x) : Nat}