How is the mapping of individual words (or symbols) to vectors is done about coqgym HOT 3 CLOSED

Yes, we use one-hot encoding of the nonterminal symbols in ASTs.
This is the vocabulary: nonterminals.
Here is how we calculate the one-hot vectors.

from coqgym.

Yes, we use one-hot encoding of the nonterminal symbols in ASTs.
This is the vocabulary: nonterminals.
Here is how we calculate the one-hot vectors.

Thanks for the reply.

Are those nonterminals part of the simple atomic tactic grammar you designed for the original paper or are those all the nonterminals available for the Coq language (thus specifying fully the Coq language e.g. programs, terms, tactics, etc)? Or what are they?

from coqgym.

They are nonterminals in the ASTs of Gallina terms, so they have nothing to do with tactics. Their corresponding implementation in Coq is in kernel/constr.ml.

from coqgym.