finding number/list of arguments?

Stream: lean4

[Siddhartha Gadgil]

If I have a theorem/definition with some arguments and a type, say

theorem silly (n m: Nat): n = m := sorry

what is the best way to retrieve the information that n and m were arguments, i.e., the definition was not

theorem silly: (n :Nat) →  (m: Nat) →  n = m := sorry

Thanks

[Notification Bot]

Siddhartha Gadgil has marked this topic as resolved.

[Notification Bot]

Siddhartha Gadgil has marked this topic as unresolved.

[Jannis Limperg]

Afaik Lean does not preserve this information after elaboration, so I don't think it can be done without defining your own variant of theorem.

[Mario Carneiro]

you can do it if you are in a linter though, since that receives the exact input syntax

[Siddhartha Gadgil]

Thanks. Does Docgen4 get this?
@Mario Carneiro I really wanted the exact input syntax. What is a "linter" here - does it have to be a plugin or can it be a regular Lean 4 (meta)-program?

[Mario Carneiro]

Linters are programs that run after each command is elaborated, they are usually used to catch common errors, like the unused variable linter

[Mario Carneiro]

What is the context in which your program is running? Is it like an autograder?

[Siddhartha Gadgil]

I am trying to extract data from mathlib4 of two kinds - the documentation strings and sequences of tactics. This question was for the first kind: log to a file definitions/theorems with docstrings whenever these are present.

[Siddhartha Gadgil]

Seems like a linter can do this. Can you point to an example of a linter?

[Siddhartha Gadgil]

And how to run a linter?

[Siddhartha Gadgil]

Okay, I see the runLinter file and some linters in Std4. I will read the code and ask about what I could not understand of it.