How to get data from an inductive type Coq

Question

I'm a little bit new to Coq, and I'm trying to do some formalization on regular grammars within Coq. Let's say I have an inductive type as follows:

Inductive rules : non_terminal -> list(non_terminal + terminal) -> Type :=
  rule1 : rules S [inr a; inl S] 
| rule2 : rules S [inr b;inl S] 
| rule3 : rules S [].

Which represents the (a* b*) grammar's derivation rules. Let's say I want to extract them for some later use. Is there any way I could do this and store it in a list of lists? e.g., I'd like a procedure that would return me [[S [inr a; inl S];S [inr b;inl S];[]]. Any other idea will be appreciated.

Thanks in advance.

Answer 1

You could try using Ltac2, which can programmatically get information about inductive types? You can also use the template-coq package/plugin. These are probably not actually what you want to be doing here, though, since it's a bit convoluted.