(* *)
(**************************************************************************)
-include "ground_2/notation/functions/downspoonstar_2.ma".
+include "ground_2/notation/functions/downspoonstar_3.ma".
include "ground_2/lib/streams_hdtl.ma".
(* STREAMS ******************************************************************)
cases n -n [ #t @t | #n #t @tl @(tls … n t) ]
defined.
-interpretation "recursive tail (strams)" 'DownSpoonStar n f = (tls ? n f).
+interpretation "iterated tail (strams)" 'DownSpoonStar A n f = (tls A n f).
(* basic properties *********************************************************)