Stream: new members
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
Julian Berman (Apr 02 2021 at 13:36):
(The middle link in particular)
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