type ('a,'b) istream
STRUCTURE
SYNOPSIS
Type of imperative streams.
DESCRIPTION
The type ('a,'b) istream is an abstract type of imperative streams. These may be created with mk_istream, advanced by next, accessed by state, and reset with reset.
COMMENTS
Purely functional streams are well-known in functional programming, and more elegant. However, this type proved useful in implementing some imperative ‘gensym’-like algorithms used in HOL.
SEEALSO
HOL  Kananaskis-14