[tromp]

Yes, let bindings would get translated like that, but there would be some straightforward optimizations done, such as size-reducing beta-reductions, which strip out unused let bindings, and inline the single-use ones, as well as the multi-use ones whose definition is smaller than the unary encoded de-Bruijn index.

[atennapel]

Yes, I wonder if these optimizations are done in the PDF. I found the BLC encoding of the lambda expressions which is 407171813 bits, about 5 mb.

[tromp]

I expect so, as the author is familiar with my tools [1] for doing these optimizations.

[1] https://github.com/tromp/AIT

[tromp]

Indeed he uses it here [1], which also gets used in lambda-8cc.

[1] https://github.com/woodrush/lambda-calculus-devkit