Bad \/ substitution in online editor leaves behind syntax-error-causing hidden zero-width characters

[Strilanc]

Go to https://leanprover.github.io/live/latest and paste the following code into the left window:

inductive NatList : Type
| nil : NatList
| cons : nat → NatList → NatList

def contains : nat -> NatList -> Prop
| _ NatList.nil := false
| x (NatList.cons e tail) := x = e \/ contains x tail

This compiles and passes, as it should.

Now put your cursor just to the right of the \/ in the line | x (NatList.cons e tail) := x = e \/ contains x tail and hit spacebar. Instead of being replaced by ∨ the \/ disappears. As icing on the cake, it hasn't actually just disappeared it has been replaced by two characters one of which is a zero-width character. So if you type \/ again there appears to be a syntax error on the \/.

Here is an example line with the zero-width character included:

| x (NatList.cons e tail) := x = e ‌\/ contains x tail

if you paste this line over the corresponding one in the code, you get a syntax error even though they look identical.

What should happen instead

First, the substitution should be fixed so that \/ becomes ∨.

Second, as defense in depth, consider using a font where unusual unprintable or zero-width unicode characters are visible.

Third, as defense in depth, lean could treat unicode whitespace characters beyond just ` and\tand\n` as also being whitespace.

[gebner]

The live version on the leanprover org is not really maintained, and we'll probably be retiring it for Lean 4 (it is Lean 3 only).

The community version is actively maintained though: https://leanprover-community.github.io/lean-web-editor/ And this bug seems to be fixed there.

[gebner]

I didn't investigate where the zero-width space is coming from (which I agree is a bug). However the standard way to write ∨ is \or, not \/.