Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Julian Berman (Apr 02 2021 at 13:36):

(The middle link in particular)

view this post on Zulip 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..

view this post on Zulip Mario Carneiro (Apr 02 2021 at 13:59):

You should just be able to copy & paste the suggestion

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Apr 02 2021 at 14:00):

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

view this post on Zulip 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