What are the most high-profile applications of Elpi besides HB? Are they packaged in opam?
(Prompted by discussion in mathcomp channel about use of Elpi for Stdpp instances, cc: @Paolo Giarrusso )
I like Trakt (https://coq.discourse.group/t/trakt-1-0-released/1558) - a generic form of zify based on Elpi.
no opam package yet though :cry:
You can find a working one here: https://github.com/ecranceMERCE/trakt/issues/3.
(I have this in my local patch repo).
There is some use of elpi in Dx https://gitlab.univ-lille.fr/2xs/dx/-/tree/main
There is also derive (which comes with coq-elpi, and which we are still improving). It has a paper attached.
In any case I like to link users in the main README of coq-elpi, so if you find more, I'm all ears
Last updated: Feb 05 2023 at 14:02 UTC