Gordon Stewart (Jan 20 2022 at 18:42): 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.
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.
Gordon Stewart (Jan 20 2022 at 19:17):Thanks, Enrico. I'll open a feature request.
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!
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 :-)
Enrico Tassi (Jan 20 2022 at 20:27):wow,. thanks!
Last updated: Oct 13 2024 at 01:02 UTC