mczify

mczify copied to clipboard

Test suite

2

We need a test suite automatically run by CI, and also extensive test cases to detect regressions. I think it makes sense to include `example.v` in it.

pi8027

- [x] `nat_of_pos`, `nat_of_bin`, `pos_of_nat`, and `bin_of_nat` (in `ssrnat.v`). - [ ] `fact_rec` and `factorial` (in `ssrnat.v`). - [ ] operators for finite ordinals (in `fintype.v`). - [ ] `prime`,...

pi8027

Performence issue

12

I have some performance issue with goals with large context. The following file takes 25s (only the last two assumptions are needed to solve it) (My real example takes more...

thery

Pair equality handling

2

Hello. I am planning to use **zify** / **mczify** as a source of inspiration for a pre-processing tool whose purpose is to prepare Coq goals before their translation to the...

ecranceMERCE