Translation Relation and Decision Procedure for CaseReduce.
The translation relation seems valid based on the Haskell code. There is a small example at the bottom of the Agda file that demonstrates the process on a single instance. For a repeated application, the compiler applies some true beta-reduction in between applications, which (deliberately) isn't implemented in these translation relations. It will be important to see if that occurs as separate phases in the implementation.
Translation Relation and Decision Procedure for CaseReduce.
The translation relation seems valid based on the Haskell code. There is a small example at the bottom of the Agda file that demonstrates the process on a single instance. For a repeated application, the compiler applies some true beta-reduction in between applications, which (deliberately) isn't implemented in these translation relations. It will be important to see if that occurs as separate phases in the implementation.
Fixes #6369