[MLton] MLton HOL

Stephen Weeks MLton@mlton.org
Wed, 2 Jun 2004 12:11:51 -0700


> The particular problem in HOL is the main function, which has
> 161,783 blocks and 257,519 variables -- the product of those two
> numbers being about 860 million.

Correction: the product of those two numbers is about 41 billion.
Now, we're not likely going to need that much space since we use a
sparse representation.  But even 1/100th would really hurt.  And of
course this rules out bit vectors.