## Stream: general

### Topic: Variables in Lean

#### Benedikt Ahrens (Jan 14 2020 at 00:22):

Hi, I would like to write the following code:

variables A B C : Prop
section simple_proof
variable a : A
variable b : B
variable c : C
theorem foobar : (A ∧ B) ∧ (A ∧ C) :=
begin
apply and.intro,
apply and.intro,
apply a,

end
end simple_proof


but see "unknown identifier 'a'". Of course, I would like to use the 'a' assumed as a variable above. Is there a way to write this?

#### Mario Carneiro (Jan 14 2020 at 00:23):

You need to include a. Lean only includes variables that are used in the statement of the theorem by default

#### Simon Hudon (Jan 14 2020 at 00:24):

Also, if you enclose your Lean code between  lean  and   , it will be prettier and more readable

#### Benedikt Ahrens (Jan 14 2020 at 00:44):

@Mario Carneiro : thanks, that's excellent to know.
@Simon Hudon : thanks, done - looks much better indeed.

Last updated: May 18 2021 at 15:14 UTC