lp:~llee454/coq-functional-algebra/master
- Get this branch:
- bzr branch lp:~llee454/coq-functional-algebra/master
Related source package recipes
Branch information
Recent revisions
- 55. By Larry D. Lee jr.
-
Added this project to GitHub. Accordingly, I placed it under Git version control. Currently, I'm developing this project using Bzr. I will try to keep all code changes in the bzr repo. and all GitHub related changes in the Git repo.
That said, I also added a LGPLv3 license to the project and added the associated header to all source files. In addition, I revised the inline comments so that they will be processed by CoqDoc. Finally, I updated the Makefile so that everything compiles under Coq version 8.8.1
- 54. By Larry D. Lee jr.
-
Merged binary tree into monoid expr. This gives monoid expr a generalized set of reduction functions. I also showed how to use these functions over a group set though groups need a more expressive datastructure than binary trees to express their structure due to the presence of a unary negation function.
- 52. By Larry D. Lee jr.
-
moved the filter 0 function to the Binary Tree module and restructured it so that it no longer relies on recursion over Term terms.
- 51. By Larry D. Lee jr.
-
Generalizing the simplification functions defined in monoid expr so that they can be applied to group expressions.
- 50. By Larry D. Lee jr.
-
Introduced notation into the Monoid Expr module to clean up expressions and added an additional unittest.
- 49. By Larry D. Lee jr.
-
Removed the top down reflection code from the Monoid module. These has been superceded by the Monoid Expr module.
- 48. By Larry D. Lee jr.
-
Upgraded the reflect tactic so that it also eliminates identity elements when simplifying monoid expressions.
Branch metadata
- Branch format:
- Branch format 7
- Repository format:
- Bazaar repository format 2a (needs bzr 1.16 or later)
