variable not visible within lemma

Stream: new members

[abaaba]

Why does variable (a: \R) is not visible in a lemma but constants (a: \R) do?

[Kyle Miller]

constant is a synonym for axiom. It's like doing def a : \R := sorry, but Lean doesn't complain about the sorry. variable is a mechanism to automatically add additional arguments to new definitions and theorems that reference them. For a theorem, if the hypotheses or conclusion do not reference a variable, it won't be included as an additional hypothesis so won't be available in a proof. You can force a variable to be included with an additional include a. (Make sure to #check the type of a lemma to see what it's doing for yourself.) https://leanprover.github.io/reference/other_commands.html#universes-and-variables