Stream: Elpi users & devs

Topic: Hint Opaque


view this post on Zulip Gordon Stewart (Jan 20 2022 at 18:42):

Is there a way to generate Hint Opaque declarations in Elpi?

I see the following API but it seems it supports only hint modes?

% -- Coq's Hint DB -------------------------------------

% Hint Mode
kind hint-mode type.
type mode-ground hint-mode. % No Evar
type mode-input hint-mode. % No Head Evar
type mode-output hint-mode. % Anything

% [coq.hints.add-mode GR DB Mode] Adds a mode declaration to DB about
% GR.
% Supported attributes:
% - @local! (default: false)
external pred coq.hints.add-mode i:gref, i:string, i:list hint-mode.

% [coq.hints.modes GR DB Modes] Gets all the mode declarations in DB about
% GR
external pred coq.hints.modes i:gref, i:string, o:list (list hint-mode).

My goal is to generate something like:

Definition r := 0.
#[global] Hint Opaque r : some_database.

view this post on Zulip Enrico Tassi (Jan 20 2022 at 19:06):

Just open an issue at https://github.com/LPCIC/coq-elpi/ and I'll add support for it, it is a reasonable request, it is just nobody needed it before.

view this post on Zulip Gordon Stewart (Jan 20 2022 at 19:17):

Thanks, Enrico. I'll open a feature request.

view this post on Zulip Gordon Stewart (Jan 20 2022 at 19:44):

Here's an issue for Hint Opaque: https://github.com/LPCIC/coq-elpi/issues/329. Thanks so much!

view this post on Zulip Gordon Stewart (Jan 20 2022 at 19:45):

BTW: coq-elpi is pretty awesome. I just started playing with it yesterday but it's already quite addictive :-)

view this post on Zulip Enrico Tassi (Jan 20 2022 at 20:27):

wow,. thanks!


Last updated: Feb 04 2023 at 02:03 UTC