Zulip Chat Archive

Stream: new members

Topic: Is this a bug?


view this post on Zulip Joe (Jul 30 2019 at 07:42):

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

view this post on Zulip Joe (Jul 30 2019 at 07:42):

Change a to b will fix it.

view this post on Zulip Joe (Jul 30 2019 at 07:43):

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

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

view this post on Zulip Joe (Jul 30 2019 at 08:04):

Oh, good to know it's already known!

view this post on Zulip Kenny Lau (Jul 30 2019 at 09:15):

Is this a bug? Yes.

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

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

view this post on Zulip Mario Carneiro (Jul 30 2019 at 23:06):

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

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

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