Stream: new members
Topic: Is this a bug?
lemma foo : true := let a := 1 in begin have : ∀θ:ℕ, (0 < θ) → a ≤ a, -- Throw the following error: -- type mismatch at application -- has_le.le a -- term -- a -- has type -- 0 < θ : Prop -- but is expected to have type -- ?m_1 : Type ? end
b will fix it.
lemma bar : true := let b := 1 in begin have : ∀θ:ℕ, (0 < θ) → b ≤ b, end
Chris Hughes (Jul 30 2019 at 07:52):
That's the letter
a bug. Something to do with the
have being parsed as
∀θ:ℕ, ∀ a : 0 < θ, a ≤ a
Oh, good to know it's already known!
Kenny Lau (Jul 30 2019 at 09:15):
a bug? Yes.
Floris van Doorn (Jul 30 2019 at 14:12):
I suggest a change to the style manual to never use
a as a variable: #1285
Note to self: it would probably be doable to write a tactic that checks whether you have used the variable name
a in declarations, to help a user spot this.
Chris Hughes (Jul 30 2019 at 14:14):
I think this is a bit strong. I rarely use
have with implies. The letter
a is used everywhere.
Mario Carneiro (Jul 30 2019 at 23:06):
The workaround style is to use
forall _:A, B instead of
A -> B in tactics
Floris van Doorn (Jul 31 2019 at 23:29):
Ok, maybe banning the letter
a everywhere is a bit of an overreaction (I was already doing it myself though, for this exact reason).
Kevin Buzzard (Aug 01 2019 at 06:50):
I went through a "no a" phase after being bitten by this early on, but it wore off...
Last updated: May 14 2021 at 06:16 UTC