HOL
HOL copied to clipboard
New Representation for Pattern Matches - Extra Features
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 #186, #58, #59, #114
More ideas are welcome.
Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.
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.