-- Spec.lean
def tileAdd (a b : List Float) : List Float :=
  List.zipWith (· + ·) a b

theorem add_correct : True := trivial