Command to get theorem type

[sorgfresser]

Added a new command that retrieves the corresponding type for a definition.

Given that the approach of separate lemmas is becoming more popular, this might be interesting to have. Consider the following:

lemma A := by <proof-of-a>

lemma B := by <proof-of-b>

theorem C := by
  have A := by <proof-of-a>

  have B := by <proof-of-b>

  <regular-proof>

which is the current approach, for example used in DeepSeekProver v2. This is inherently redundant. Importantly, the proof of A, B is not necessary in C.

Instead, one can now write

theorem C (hx: type of A) (hy: type of B) := by <regular-proof>

and compose via

exact C A B

[augustepoiroux]

This is an interesting feature in my opinion. REPL has extraction capabilities centered around tactics, and I believe that adding some for declarations could be nice. https://github.com/leanprover-community/repl/pull/96 is related to this in that sense. Regarding this PR, maybe it could be integrated directly into Command (i.e. "cmd" in JSON) as a parameter instead of having to do a separate query (similar to the allTactics parameter). What do you think?

[sorgfresser]

@augustepoiroux thanks for the feedback! I moved this to a flag declTypes now. Let me know if that's a better interface :)