## Stream: new members

### Topic: printing lemma statements

#### Michael Beeson (Oct 16 2020 at 04:00):

I would like to have Lean print out the statements and names of all the lemmas and theorems I have proved.
How can I do that?

#### Kevin Lacker (Oct 16 2020 at 04:05):

I am also curious whether this is possible

#### Yury G. Kudryashov (Oct 16 2020 at 04:06):

How exactly do you define "I have proved"?

#### Yury G. Kudryashov (Oct 16 2020 at 04:07):

All lemmas in the current environment? All lemmas in the current file? Something else?

#### Kevin Lacker (Oct 16 2020 at 04:08):

or do you just want to know what they are, rather than having Lean itself do it, in which case you can do grep lemma your_code.lean :wink:

#### Michael Beeson (Oct 16 2020 at 04:30):

grep doesn't do it because some of the lemmas are on two or more lines. That only gives me the first line.
I mean all the lemmas in the current environment.

#### Michael Beeson (Oct 16 2020 at 04:31):

Today I proved duplicates of two lemmas I proved weeks ago, having forgotten that I already proved them. Yikes!

#### Michael Beeson (Oct 16 2020 at 04:33):

I have about 80 lemmas. Each one has a name in the Latex file, and a number that latex assigns it, and a name in the Lean file of the form "lemma43" that corresponds with the number in the pdf file that Latex makes. This is a clerical nightmare.

#### Michael Beeson (Oct 16 2020 at 04:34):

Since I refer to the pdf while formalizing the proof, that's why I made the Lean names correspond to the numbers in the pdf file.

#### Yury G. Kudryashov (Oct 16 2020 at 04:37):

Note that the lemmas in the current environment include lots of lemmas from stdlib (and mathlib if you import it).

#### Yury G. Kudryashov (Oct 16 2020 at 04:37):

Do you want to have the list of lemmas from the current repository?

#### Alex J. Best (Oct 16 2020 at 04:39):

Heres a simple user command that prints name + statement of all decls in the file (not very well tested), this is in the file not the environment, you can remove the filter part if you want them all.

import tactic.basic
reserve notation #file_decls

-- examples
lemma bar (n : ℕ) (h1 : 0 < n) : 0 < n := sorry
lemma baz (n : ℕ) : 0 < n + 1 := sorry

open tactic
setup_tactic_parser
meta def file_decls : tactic (list (name × expr)) := do
e ← get_env,
let l := e.filter (λ d, e.in_current_file d.to_name),
return (l.map (λ d, ⟨d.to_name, d.type⟩))
@[user_command] meta def file_cmd (_ : parse \$ tk "#file_decls") : lean.parser unit :=
trace file_decls.

#file_decls


#### Kevin Lacker (Oct 16 2020 at 04:46):

you can also use awk to do something like grep but across multiple lines: awk '/lemma/,/:=/' yourfile.lean

#### Michael Beeson (Oct 16 2020 at 05:58):

Kevin, that awk command prints out a zillion lines within the proofs where I have given an exact proof using :=
so it doesn't serve the desired purpose. Probably I can make it fancier and get only lines that begin with 'lemma' and subsequent lines up to := .Nice idea.

#### Michael Beeson (Oct 16 2020 at 05:59):

Has anyone thought about how one might fold up the tiniest inferences, leaving only the "important" lines,
and then scrape them off in a form that could be pasted into LaTeX?

#### Johan Commelin (Oct 16 2020 at 06:37):

@Michael Beeson if you speak Python, you might want to look at lean-formatter

Last updated: May 17 2021 at 21:12 UTC