Re: [Hol-info] recspace

[Michael N. <Mic...@ni...>]

Mike Gordon wrote:
> Anyone know what recspace is (see question below)? I've not come
> across it before.

Recspace is the type used by the datatype package to support the 
creation of algebraic types.  It's basically a type of trees.  Users 
shouldn't rely on it at all, which is why it's not documented.  (In 
other words, the implementation of the datatype package might change, 
and that type might disappear.)

If you are after types of trees, there are a couple in the distribution 
that won't be lost (though they're minimal and need extending): inftree, 
a type of potentially infinitely branching algebraic tree; and lbtree, a 
type of "lazy" (i.e., co-algebraic) binary trees.

Michael.