Sam Tobin-Hochstadt

If the further thoughts on this are about the changes to Racket proposed by @thinkmoore, can we keep them in this discussion so that they're archived/accessible to others of us...

The functions here: https://docs.openssl.org/3.1/man3/d2i_PrivateKey/#copyright seem to autodetect the key format, but that would require upgrading to v3.

There's a comment in the file saying that terms with duplicate variables falsify the theorem, but this is a different issue.

I don't think just switching to unary functions is enough, you probably need to take out numbers as well. This term: `((lambda (z) z) (lambda (x) (5 x))))` is a...

I'm not sure what you mean. Consider the following: ``` (define bad-term (term ((lambda (z) z) (lambda (x) (5 x))))) (traces s-->β bad-term) (traces s-->βη bad-term) (traces -->βη bad-term) ```...

The Redex book part 1 stops having eta as soon as it gets to ISWIM, and doesn't ever have multi-argument functions, avoiding these problems. In fact footnote 2 (p49) says...

Well, there's both the ordering issue and the fact that the metafunction returns immediately when given a lambda, so `(lambda (x) (5 x))` doesn't reduce even though it has an...

Running this command: ``` $ raco fmt -i recspecs/main.scrbl ``` in a checkout of https://github.com/samth/recspecs at the current HEAD (or revision ce25f983c7fece4cdf216159b609484c03d8b39a) will produce the error.