Parsing strings with `def` or `theorem` keywords

Stream: metaprogramming / tactics

[Anand Rao]

I would like to be able to parse strings like "theorem foo (m n : ℤ) : m + n = n + m", which contain keywords such as theorem or def, to lean3 expressions.

I am aware that standalone expressions like ∀ (m n : ℤ), m + n = n + m can be parsed by using lean.parser.with_input interactive.types.texpr, and I tried inspecting the source for similar functions but could not infer much. I expect that lean should have a built-in mechanism of converting a statement like theorem foo (m n : ℤ) : m + n = n + m to theorem foo : ∀ (m n : ℤ), m + n = n + m (where all the parameters are pushed to the right of the colon with universal quantification), because I usually see the latter when I #check theorem names.

Is there a way for me to parse strings that contain theorem or def keywords? Alternatively, is there an in-built function that pushes all the parameters to the right of the colon, so that I can simply discard everything to the left of the colon and run the usual `lean.parser.with_input interactive.types.texpr?

[Eric Wieser]

Can you elaborate a bit on your motivation?

[Anand Rao]

This is meant for checking the output of a language model.

[Eric Wieser]

You could write the string out to a file, append a short metaprogram to inspect the definition it generates and dump it to stdout, and then use io.cmd ["lean", your_file] to get the result

[Eric Wieser]

Is the language model written in lean itself?

[Eric Wieser]

Maybe this answers your question:

import tactic.core

run_parser do
  lean.parser.emit_command_here "def foo : ℕ := 1",
  d ← tactic.get_decl `foo,
  tactic.trace d

[Eric Wieser]

If you don't even know what the name of the theorem that the language model output was, you could list all the existing names, then emit the model code, then see what new names appeared