Is this a bug?

Stream: new members

[Joe]

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

[Joe]

Change a to b will fix it.

[Joe]

lemma bar : true :=
let b := 1 in
begin
  have : ∀θ:ℕ, (0 < θ) → b ≤ b,
end

[Chris Hughes]

That's the letter a bug. Something to do with the have being parsed as ∀θ:ℕ, ∀ a : 0 < θ, a ≤ a

[Joe]

Oh, good to know it's already known!

[Kenny Lau]

Is this a bug? Yes.

[Floris van Doorn]

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]

I think this is a bit strong. I rarely use have with implies. The letter a is used everywhere.

[Mario Carneiro]

The workaround style is to use forall _:A, B instead of A -> B in tactics

[Floris van Doorn]

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]

I went through a "no a" phase after being bitten by this early on, but it wore off...