Kazuhiko Sakaguchi

My main concern regarding standalone preprocessing tactics like `ppsimpl`, `zify`, `trakt`, and `simp` (of Lean) is that we often seem to make the whole automated proving procedure slower by piling...

Recently, I started to generalize `interval.v` on top of `order.v` and proved that intervals on a `latticeType` are a (non-distributive) lattice, where the meet operator is the intersection and the...

After spending a day for this, I have obtained 4 non-distributive lattice structures: - `ndlatticeType`: plain non-distributive lattices, - `ndblatticeType`: non-distributive lattices with bottom, - `ndtblatticeType`: non-distributive lattices with bottom...

@hivert > Excellent ! Each times I'm trying to insert something inside the hierarchy, I end up in a nightmare with canonical wishing there where really some ghostbuster around ;-)...

@strub @hivert I put my non-distributive lattice structures branch as a PR math-comp/math-comp#388. So if you find something wrong, missing things, etc., please report them as comments of that PR....

We still need extensive test cases to detect regressions. It would also be nice to have more examples demonstrating the usefulness of mczify. Contributions are welcome.

I added some more test cases, but there are still many missing cases: https://github.com/math-comp/mczify/blob/8481446a34ee53cf24639210877ed9f7dd1dcf92/examples/test_ssreflect.v

@CohenCyril Great! I will take a look tomorrow. I probably prefer to keep them in a separate file because it is rather a "meta" result.

Thanks for your contribution! I checked your codes, and found some issues. Please fix these issues: - Newline character is omitted in the last line of some files. (E.g. ChurchNumerals.agda)...

> It fails with `x ident` but not with `x binder`. Thanks. After looking at the reference manual, it seems more appropriate to use `x name`, but the above example...