Can't use '' as infix operator

[semorrison]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

We'd like to use '' as an infix operator in mathlib; we use it for the image of set. However it generates a missing end of character literal whenever used:

Steps to Reproduce

def Set (α : Type u) := α → Prop

def image (f : α → β) (s : Set α) : Set β :=
  fun b => ∃ a, s a ∧ f a = b

infixl:80 " '' " => image

example {f : α → β} {s : Set α} {y : β} : f '' s = f '' s := rfl -- Errors on `f '' s` with `missing end of character literal`.

Expected behavior:

No error.

Actual behavior:

missing end of character literal

Versions

Lean (version 4.0.0-nightly-2022-12-05, commit 0b243f0, Release)

Additional Information

As reported in zulip.

[Kha]

I guess there is a quick and a thorough solution.

• quick: do not invoke char token parser if second character is also '. Should only regress error message on '' without notation
• thorough: replace built-in token parsers with generic variable-length, longest-parse token parsing

[kbuzzard]

(comment moved to Zulip)

[digama0]

@Kha I think the quick solution is better for the immediate issue (we had to add a workaround for the port but it would be good to remove it before we forget). The "thorough" solution sounds like a bit of a project and I think only you would be able to do it, so I'd rather not bank on it but please try it if you are motivated to do so.

[digama0]

By the way, the reason lean 3 can parse this is that it registers ' as a token, and then does a longest match tokenization with all the tokens to do the initial dispatch to char parser, string parser, mod doc parser etc. If there is no '' token, then it will parse ' and then go to the char parser (which reads it as an unterminated char literal and gives an error). But if a '' token is registered then it gets treated as such.