New Representation for Pattern Matches - Extra Features

[thtuerk]

This is a subtask of issue #285.

Implement extra features for pattern matches. Current ideas:

• improved support for arithmetic expressions
• improved support for list patterns
• better support for creating equations (esp. using exhaustiveness checks)
• flattening patterns
• integrate with function definition package to address issues like Quantification over Define's result #186, Define disallows underscores on the rhs, even in patterns #58, Define sometimes requires eta-expanded recursive calls #59, Annoyance with patterns in Define #114

More ideas are welcome.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

[thtuerk]

There is now better support for creating equations. This also helps with the function definitions issues, but more work is needed there. If you are interested, read the new Section "6.8.4. Lifting case expressions" in the description manual.