Files in examples/ have two roles:
- examples showing the features of Algebra Tactics, and
- test-suite.
I see the following three issues:
- Currently, these two things are kind of mixed. So, they are not very friendly to the users who want to discover the features.
- Checking
ring_examples.v and field_examples.v requires uncommenting Require Imports. (This way we can test the "no check" option.)
- As the test suite, they are not very exhaustive either.
Files in
examples/have two roles:I see the following three issues:
ring_examples.vandfield_examples.vrequires uncommentingRequire Imports. (This way we can test the "no check" option.)