Zulip Chat Archive

Stream: new members

Topic: why doesn't this work?


view this post on Zulip Alex Kontorovich (Apr 22 2020 at 13:46):

Can someone please help explain why the following:

lemma sum_plus_one1 (F:   ) (m: ) : sum (range (nat.succ m)) F = sum (range m) F + F m:=
begin
  exact sum_range_succ' F m,
end

doesn't work, and gives an error that says:

invalid type ascription, term has type
sum (range (nat.succ m)) F = sum (range m) (F ∘ nat.succ) + F 0
but is expected to have type
sum (range (nat.succ m)) F = sum (range m) F + F m

WTF?!?! Where did that "F ∘ nat.succ" come from??? The lemma is verbatim what the tactic is asking for...? Thank you!

view this post on Zulip Reid Barton (Apr 22 2020 at 13:47):

Well, looking at the error message, it seems that sum_range_succ' splits off the first element of the sum, not the last.

view this post on Zulip Alex Kontorovich (Apr 22 2020 at 13:48):

I don't follow? I literally copied and pasted what it said was "is expected to have type" into the lemma statement?

view this post on Zulip Reid Barton (Apr 22 2020 at 13:48):

You're reading the error message backwards, then.

view this post on Zulip Alex Kontorovich (Apr 22 2020 at 13:49):

Argh!!! You're right. Thanks.

view this post on Zulip Alex Kontorovich (Apr 22 2020 at 13:49):

Meant to use sum_range_succ instead

view this post on Zulip Reid Barton (Apr 22 2020 at 13:50):

GHC has a similar error message and it seems to confuse a lot of people there, too, though I never understood how. I guess it is like one of those optical illusions, where once you see it one way it is tricky to see it the other way.

view this post on Zulip Reid Barton (Apr 22 2020 at 13:51):

I think they may have reworded this error message in GHC recently, actually.

view this post on Zulip Reid Barton (Apr 22 2020 at 13:52):

I think it's the phrase "expected" type that trips people up


Last updated: May 11 2021 at 14:11 UTC