Reorganize the test-suite and examples - Githubissues

math-comp / algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components

33 stars 2 forks source link

Reorganize the test-suite and examples #91

Open pi8027 opened 1 year ago

pi8027 commented 1 year ago

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.