Zulip Chat Archive

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) :=
    apply and.intro,
      apply and.intro,
      apply a,

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: Aug 03 2023 at 10:10 UTC