Documentation

Lean.Compiler.LCNF.SimpCase

This pass provides simplifications for cases statements at the impure level. The LCNF pure simplifier must restrict itself when touching cases statements as to not destroy information for the reset-reuse insertion. However, this pass runs after reset-reuse insertion and can thus be much more liberal in its application of cases simplifications.

In particular we perform:

Note: Currently the simplifier still contains almost equivalent simplifications to the ones shown here. We know that this causes unforseen behavior and do plan on changing it eventually.