Declaration information extraction

[augustepoiroux]

Extract various information about declarations in commands through the "declarations": true attribute:

• Kind: definition, theorem, inductive, ...
• Modifiers: docstring, visibility (private, protected, ...), computeKind ("meta", "noncomputable", ...), recKind ("partial", "nonrec", ...), isUnsafe, and attributes
• Type (= conclusion for theorems)
• Binders (= variables/hypotheses for theorems)
• Signature (= binder + type)
• Value (= proof for theorems)
• Scope information: current namespace, declared variables, ...

TODO:

• Improving the extraction of used constants.
• Improving the extraction of declaration full names (they should match the ones in the environment).

Contributions and feedback are welcome!

Notes:

• Inspired and similar to the declaration extraction process from jixia
• Take a slightly different approach to Command to get theorem type #101 for extracting declaration information
• This PR depends on Introduce incremental processing of the commands #109 (and is built on top of Automated prefix state sharing optimization #110 in the current state).