Printing axioms, theorems, definitions etc. in file

Stream: new members

[Josh Chen]

Hi all, is there already a tool that outputs a list of axioms, theorems, definitions, etc. defined in a .lean file? I have to do assignment marking and want to avoid having to roll my own version of such a thing, if possible.

[Julian Berman]

Possibly this comment from yesterday in another stream is helpful: https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning.20for.20Theorem.20Proving/topic/Lean.20client.20for.20Python/near/232835269

[Julian Berman]

(The middle link in particular)

[Josh Chen]

Thank you! :) I really would like to be able to batch this without having to learn Lean metaprogramming just right now, but it's a start..

[Mario Carneiro]

You should just be able to copy & paste the suggestion

[Mario Carneiro]

but most access to lean data structures is done using the metaprogramming stuff so you can't really avoid it

[Bryan Gin-ge Chen]

That user command seems worth PRing to mathlib. cc: @Alex J. Best

[Alex J. Best]

@Bryan Gin-ge Chen thanks, I won't have much lean time for the next couple of weeks, I made #7003 to track this so I don't forget though, I'll try and make the PR then (of course if anybody does so in the meantime I won't object!). Probably it won't take too long but thinking about the most useful way to format the output might take a few minutes.