(n > 0) as a variable declaration

Stream: new members

[Mike Shulman]

When my students want to prove something about a positive natural number, a number of them seem to naturally write

theorem foo (n : ℕ) (n > 0) : ...

forgetting to give a name to the hypothesis that n > 0. Surprisingly to me, Lean actually accepts this syntax, but it appears that it interprets (n > 0) to mean (n : ℕ) (H : n > 0), so that foo actually ends up with two arguments named n, one of which is positive. I will restrain myself from opining on whether I think this is a good design choice and merely ask, where is it documented and what exactly are the rules governing it? I couldn't find it on a quick look through the reference manual. Is it something like "if when expecting a variable declaration Lean finds instead just a bare term of the form x R a where R is a binary relation and x is a variable name, it interprets this as meaning (x : A) (H : x R a)"?

[Mario Carneiro]

It is an outgrowth of the hack to support \forall n > 0, p n, \exists n > 0, p n etc

[Mario Carneiro]

the rule is that (x1 ... xn R a) is a binder, and is expanded to (x1 : _) (H : x1 R a) ... (xn : _) (H : xn R a)

[Mike Shulman]

Thanks. Is it documented anywhere?

[Mario Carneiro]

not that I know of

[Mario Carneiro]

well, there is this: https://github.com/leanprover-community/lean/blob/1f4fec79d25c9a357871f0df896f01b24fbfc35c/src/frontends/lean/parser.cpp#L1037-L1044