I would like to be able to extract a datapoint of definitions and theorem statements which includes the recursive dependencies of each datapoint. I'm imagining giving each datapoint (in json) a unique identifier (perhaps its kernel name) and having a list of direct dependencies.
I would also like to have a mapping of datapoints to which module they come from (From foo Require bar.baz or w/e).
Ideally, we could separate dependencies of the theorem statements from dependencies of their proofs, but this is not necessary. Also, ideally, we'd be able to get the notation & ltac dependencies, but this seems much harder.
References that might make this easier:
I would like to be able to extract a datapoint of definitions and theorem statements which includes the recursive dependencies of each datapoint. I'm imagining giving each datapoint (in json) a unique identifier (perhaps its kernel name) and having a list of direct dependencies.
I would also like to have a mapping of datapoints to which module they come from (
From foo Require bar.bazor w/e).Ideally, we could separate dependencies of the theorem statements from dependencies of their proofs, but this is not necessary. Also, ideally, we'd be able to get the notation & ltac dependencies, but this seems much harder.
References that might make this easier: