RedPRL / cooltt

😎TT
http://www.redprl.org/
Apache License 2.0
219 stars 16 forks source link

🚫🆔 Nameless schemes for `BindSym`, `LetSym` and `DimProbe`? #335

Closed favonia closed 2 years ago

favonia commented 2 years ago

(This was a GitHub Discussion.)

When working on the #211, I noticed that cache misses were due to the global new names used in DimProbe. Perhaps it's possible to use nameless schemes for these binders and/or symbols. For now, the SMT experiment in #211 is paused and caching is not needed.