Thorsten Altenkirch (Feb 17 2021 at 15:10):
Think I have used variables in proofs before but today nothing works. What is wrong:
variable P : Prop variable p : P example : P := p example : P := begin exact p, end
I have boiled it down. Why does it say unknown identifier here?
Heather Macbeth (Feb 17 2021 at 15:14):
include p example : P := begin exact p, end
Heather Macbeth (Feb 17 2021 at 15:15):
If I understand correctly, by default Lean only brings into tactic mode the variables which appear in the hypotheses or conclusion.
Johan Commelin (Feb 17 2021 at 15:16):
omit is the evil twin of
Thorsten Altenkirch (Feb 17 2021 at 15:16):
Thank you. Actually I have used this before and forgot about it... :-( This just drove me mad.
Johan Commelin (Feb 17 2021 at 15:18):
Ooh, just run
omit mad to unmad yourself again :rofl:
Jeremy Avigad (Feb 17 2021 at 18:41):
The reason that Lean makes you include
p explicitly is that a tactic block is really a metaprogram, there is no way for the parse to figure out what
p really means. You can have tactics that add things to the context, delete things from the context, and rename things in the context. So Lean doesn't even try to guess what you want to include (even though with
exact p is seems pretty obvious).
Thorsten Altenkirch (Feb 18 2021 at 10:31):
I noticed that once I am including a variable type inference fails because I suppose it also tries to use the new assumptions. Basically I only wanted to use variables as a replacement for a proof I don't want to do in the moment - I guess I better use sorry in this case?
Last updated: May 10 2021 at 17:39 UTC