HOL icon indicating copy to clipboard operation
HOL copied to clipboard

New Representation for Pattern Matches - Extra Features

Open thtuerk opened this issue 9 years ago • 1 comments

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.

thtuerk avatar Aug 30 '15 09:08 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.

thtuerk avatar Jan 24 '17 10:01 thtuerk