InfoTrees and CommandInfo

Stream: general

[Riyaz Ahuja]

Quick question: is it guarunteed that every Lean.Elab.InfoTree (as extracted by something like CompileModule module) has exactly one CommandInfo node, or is it possible to have multiple in one infotree? If so, what kind of situation would cause that to happen?

For some context, I'm trying to split a file into its constituent theorems, and I was wondering if it is robust enough to just split on the infotrees generated by compiling the module. It seems like it from the little tests I've done, but I want to make sure there's no weird edge cases before committing to it.

[Damiano Testa]

Would something like

run_cmd
  let cmd1 ← `(command|#exit)
  let cmd2 ← `(command|end)

have more than one CommandInfo node?

[Damiano Testa]

I would also look into mutual blocks for sources of potential multiple CommandInfos.