defining notation

Stream: new members

[Patrick Thomas]

Am I defining this notation wrong? It seems like maybe it is interfering with the notation for lists?
Screenshot-from-2022-05-23-20-49-49.png

[Kyle Miller]

Could you post a code block rather than a screenshot? You could also post the URL of the web editor, since it includes the contents of the text area.

[Patrick Thomas]

https://leanprover-community.github.io/lean-web-editor/#code=import%20logic.function.basic%0A%0A%23check%20%5B%20%22x%22%20%5D%0Anotation%20%20%60%5B%60%20a'%20%60%E2%86%A6%60%20v%20%60%5D%60%20f%20%3A%3D%20function.update%20f%20a'%20v%0A%23check%20%5B%20%22x%22%20%5D

[Patrick Thomas]

I wasn't sure how to escape the backticks in zulip.

[Patrick Thomas]

I guess they show up if I put them in a code block.

import logic.function.basic

#check [ "x" ]
notation  `[` a' `↦` v `]` f := function.update f a' v
#check [ "x" ]

[Kyle Miller]

Thanks for the code block. I think you're right that it's interfering with list notation. That's defined using

notation `[` l:(foldr `, ` (h t, list.cons h t) list.nil `]`) := l

and it seems likely that the parser wouldn't be able to disambiguate between your notation and this foldr pattern.

[Kyle Miller]

Here's a potential workaround:

notation a ` ↦ `:25 v := λ f, function.update f a v

#eval (1 ↦ 3) id 0
-- 0
#eval (1 ↦ 3) id 1
-- 3

[Kyle Miller]

I set the precedence of the arrow to 25 just because that's the precedence of implication.

[Patrick Thomas]

Thank you!