Zulip Chat Archive

Stream: general

Topic: linter fails

Yaël Dillies (Sep 27 2021 at 16:09):

This linting is funny. One of the tactics failed to typecheck!

Eric Wieser (Sep 27 2021 at 16:16):

Maybe you hit a hash collision in the cache?

Yaël Dillies (Sep 27 2021 at 16:19):

Oh, how do you know that?

Floris van Doorn (Sep 27 2021 at 17:14):

I'm worried that Lean is confused by the new notation introduced in this PR.

Bryan Gin-ge Chen (Sep 27 2021 at 17:21):

That was my first guess as well. Could you try putting the notation in a locale?

Floris van Doorn (Sep 27 2021 at 17:23):

Yeah, the problem is that the following notation make other notations that start with [ unusable.

notation `[` a ` ≤ ` b ` ≤ ` c `]` := btw a b c
notation `[` a ` < ` b ` < ` c `]` := sbtw a b c

I think that the story is as follows: after seeing [ Lean has to decide what this notation is going to mean. It can overload notation, but only if the parser is the same for the different overloads (which is not the case for btw, sbtw, and list.nil). If the future parsing is different, then it has to make a choice, and in this case it just chooses the last declared notation (the one for sbtw).