I wonder if there is a way to query the strategy (opaque, transparent, in between) of a symbol in Ltac2.

Not that I know of.

You can do that in elpi, and call an elpi tactic via ltac1 (horrible, but ...)

https://github.com/LPCIC/coq-elpi/blob/e4bf0b0b3e092b16c89b4e49d64523902fe24d13/coq-builtin.elpi#L1396

If you tell me the "API" you want I can easily write a few lines for you. Given the bridge, the output has to be a term I guess

Alternatively, you cal look at the OCAML code implementing these APIs, and take inspiration to write ltac2 bindings

@Enrico Tassi : thanks! Essentially in Ltac2 I have a `constr`

which is a reference or a `reference`

(one can convert between the two, so I don't care) and want an Ltac2 integer, but a constr with a Gallina Z or positive is fine (I have conversion functions for these).

@Enrico Tassi : actually looking at this post (https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Custom.20reduction/near/298778993) I might be more interested in the "original opaqueness", that is if a symbols was defined with Qed or not.

I'm a bit in a hurry, here a draft:

```
From elpi Require Import elpi.
Elpi Tactic is_qed_opaque.
Elpi Accumulate lp:{{
pred is-opaque i:gref, o:term.
is-opaque (indt _) {{ true }}.
is-opaque (indc _) {{ true }}.
is-opaque (const C) {{ true }} :- coq.env.const C none _, !.
is-opaque (const _) {{ false }}.
solve (goal _ _ _ _ [trm T] as G) GLS :-
coq.term->gref T GR,
is-opaque GR B,
refine B G GLS.
}}.
Elpi Typecheck.
Tactic Notation "is-opaque" uconstr(c) := elpi is_qed_opaque ltac_term:(c).
Lemma x : unit. Proof. exact tt. Qed.
Lemma y : unit. Proof. exact tt. Defined.
Goal True.
pose (b1 := (ltac:(is-opaque nat))).
pose (b2 := (ltac:(is-opaque S))).
pose (b3 := (ltac:(is-opaque x))).
pose (b4 := (ltac:(is-opaque y))).
pose (b5 := (ltac:(is-opaque 37))).
pose (b6 := (ltac:(is-opaque plus))).
Abort.
```

Last updated: Apr 21 2024 at 01:02 UTC