HigherOrderCO / Kind

A modern proof language
https://higherorderco.com
MIT License
3.58k stars 142 forks source link

Kdl compilation genereates needless/unused terms #404

Closed developedby closed 4 months ago

developedby commented 2 years ago

The kind to kdl compiler currently generates code that sometimes contains lets that are never used, with an unbound variable, lets binding a variable to another (useless indirection) and dups where at least one of the bound variables is unused.

The first two I'm certain it happens and will add some examples later, the third one I'm not so sure, but vaguely remember it happening before.

algebraic-dev commented 1 year ago

I think that it could be an optimization pass for all backends not only for KDL.