Two new versions of SASyLF have been released on the SourceForge download site:
https://sourceforge.net/projects/sasylf/files/Releases/1.2.6: bug fixes on the "stable" 1.2.X branch, and a few features
1.3.1: All 1.2.6 + new features beyond 1.3.0.
- abstract modules
i.e. define a semi-group over an unknown data type and unknown associate operator
- "or" clauses:
e.g.
exists n1 > n2 or n1 = n2 or n2 > n1 .
- "use induction on x, y, z"
Lexicographic induction variables
- partial case analysis -- handle special cases out of line
The last two new features are featured in a new example: cut-elimination.slf in the examples folder.
In the coming week, the Wiki documentation will be updated with the new features.
Please post any bugs found on GoogleCode:
http://code.google.com/p/sasylf/issues/listThanks to my ETH Zurich students who have helped by finding bugs for me to fix.
Best regards,
John