kinds of metavariables

[fpvandoorn]

What question should the reference manual answer?

What kind of metavariables are there (synthetic opaque, etc.)? What are their precise descriptions and differences? How do the different versions come into existence? Maybe in scope: what tactics/meta-definitions are able to assign which metavariables (or in what way do they handle the different kinds of metavariables differently)?

Additional context
This Zulip post states "isDefEq does not assign synthetic opaque metavariables". It would be nice if after reading this section I could (1) learn what this precisely means and ideally (2) allow me to predict whether another meta-def would or would not make such assignments.

[david-christiansen]

Thanks, this will be a valuable distinction to cover once we get into metaprogramming and language extension.