Variables in Lean

Stream: general

[Benedikt Ahrens]

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]

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

[Simon Hudon]

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

[Benedikt Ahrens]

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