I mostly run SBCL on FreeBSD. I'm interested in CLX
I've been dabbling in Theorem Proving and have written a pattern matching macro, tuned to this application. I've implemented it using typecase and destructuring-bind. I've implemented it again more directly.
I like the second version better and want to write it up nicely, as an example of writing a tricky macro.