Chun Tian

Hmmm, maybe I wrongly blamed `LET_ELIM_TAC` code. The result after `rw []` looks like `LET_ELIM` has already been applied - all the `LET`-bindings are indeed eliminated. What's really unexpected is...

Hi, I don't think Quicklisp (or ASDF) supports loading specific versions of Lisp packages. And why you have to use an old version of usocket?

> I think it's arguable either way. I'd expect the big multiplicative blobs to get normalised so that they turn into things like the example that works. I will check...

I think currently the normalizer of real expressions thinks `-1 / x` cannot be further simplified, because it's "minimal". I think it makes sense to let it go further to...

LaTeX is still the best option for producing high-quality PDF documents for printing purposes (I believe there are still people who print the manual and read it as a book)....

Sorry, the regression tests were not well-maintained for all OS/CL combinations. I will see what I can do.

> Oh, I forgot to add that I made this minor local change to usocket: > > ``` > diff --git a/backend/openmcl.lisp b/backend/openmcl.lisp > index 785bca9..b3f3321 100644 > --- a/backend/openmcl.lisp...

Hi, I will make a new release soon, once I got feedback from another user (on another bugfix). Good to know the existence of `quick-patch`.

I want to remind you that HOL theories are essentially compiled libraries of SML, and the entire HOL system can be seen as a library of SML. The fact that...

Hello @myreen, if this is the algorithm for finding the shortest paths between nodes in a weighted graph, I think I failed to see the "weighted graph" here - what's...