Pierre-Yves Strub
Pierre-Yves Strub
Hi, With Xavier Allamigeon, we also need non-distributive lattices, inf-semi lattices and graded posets (and some combinations of the 3 previous ones). I just started adding graded posets to order.v....
> @pi8027 > > > So now I'm motivated to add the non-distributive lattice structure to MathComp. I intend to do it after [math-comp/math-comp#270](https://github.com/math-comp/math-comp/pull/270) is merged. > > @hivert >...
Ok, thx. I am discovering Coq ELPI at the same time.
@pi8027 That was fast. In that case, I am going to rebase my graded poset structure on top of your branch and will start using the non-distributive bottom lattices ASAP...
A few months ago (if not less), I asked for pulling out the `distr` library so that I can maintain it (I think that nearly of the contents of this...
For information, you can extract the keywords with: ``` ./scripts/srctx/keywords -m raw < src/ecLexer.mll ```