Zulip Chat Archive

Stream: general

Topic: Variables in Lean


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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