## Stream: new members

### Topic: Printing axioms, theorems, definitions etc. in file

#### Josh Chen (Apr 02 2021 at 13:27):

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 (Apr 02 2021 at 13:35):

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

#### Josh Chen (Apr 02 2021 at 13:52):

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 (Apr 02 2021 at 13:59):

You should just be able to copy & paste the suggestion

#### Mario Carneiro (Apr 02 2021 at 14:00):

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

#### Bryan Gin-ge Chen (Apr 02 2021 at 14:00):

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

#### Alex J. Best (Apr 02 2021 at 15:49):

@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.

Last updated: May 13 2021 at 22:15 UTC