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
``` , 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