Zulip Chat Archive

Stream: new members

Topic: variable not visible within lemma

abaaba (Nov 05 2021 at 04:09):

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

Kyle Miller (Nov 05 2021 at 04:40):

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

Last updated: Dec 20 2023 at 11:08 UTC