wish: syntax about coq-elpi HOT 5 CLOSED

When real user extensible attributes will be there:

#[elpi(mixin)] Record ....
#[mixin] Record ...
#[factory] Record ...  #[factory] End.

from coq-elpi.

It seems Cyril found a simpler way

from coq-elpi.

Nop, my solution only works because we do not have parameters yet!

from coq-elpi.

I checked the code and while parsing things is doable the whole "globalization" is a mess, hard to reuse.
In particular the two phases (intern and interp) are mixed. If we really need this feature, quite some work on the Coq side is needed as well.

from coq-elpi.

maybe I could write it as a (fun ... => ...) or (forall ..., ...), if only I could omit the fun/forall keyword, => symbol and parenthesis 😆 ... well I would like to parse a telescope...

from coq-elpi.