Pipe character "|" not working to denote divides

Stream: new members

[Luis Berlioz]

In the TPiL book the following code appears in the exercises in section 4.6:

namespace hidden

def divides (m n : ℕ) : Prop := ∃ k, m*k = n

instance : has_dvd nat := ⟨divides⟩

def even (n : ℕ) : Prop := 2 | n

end hidden

I get two errors:
pointing at the 2: Failed to synthesize type class instance for n : nat
and at the pipe symbol "|": command expected
I noticed that the same code works in the Lean Web Editor.
Locally, I am running lean on emacs lean-mode.
Any ideas on how to fix this issue?

[Mario Carneiro]

It's not a pipe symbol, it's a unicode \|

[Mario Carneiro]

Not one of our best choices

[Luis Berlioz]

yikes! That works.
Thanks

[Yury G. Kudryashov]

@Mario Carneiro BTW, is there any reason to use U+2225 PARALLEL TO for norm instead of U+2016 Double Vertical Line?

[Mario Carneiro]

ask @Patrick Massot

[Mario Carneiro]

I don't think we are big on unicode semantic information, we just use whatever looks good