mk_istream : ('a -> 'a) -> 'a -> ('a -> 'b) -> ('a,'b) istream
STRUCTURE
SYNOPSIS
Create a stream.
DESCRIPTION
An application mk_istream trans init proj creates an imperative stream of elements. The stream is generated by applying trans to the state. The first element in the stream state is init. The value of the state is obtained by applying proj.
FAILURE
If an application of trans or proj fails when applied to the state.
EXAMPLE
The following creates a stream of distinct strings.
   - mk_istream (fn x => x+1) 0 (concat "gsym" o int_to_string);
   > val it = <istream> : (int, string) istream

COMMENTS
It is aesthetically unpleasant that the underlying implementation type is visible.

See any book on ML programming to see how functional streams are built.

SEEALSO
HOL  Kananaskis-14