## Stream: new members

### Topic: Pipe character "|" not working to denote divides

#### Luis Berlioz (Jul 19 2019 at 19:12):

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 (Jul 19 2019 at 19:13):

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

#### Mario Carneiro (Jul 19 2019 at 19:14):

Not one of our best choices

#### Luis Berlioz (Jul 19 2019 at 19:14):

yikes! That works.
Thanks

#### Yury G. Kudryashov (Jul 21 2019 at 04:17):

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