Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jul 19 2019 at 19:13):

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

view this post on Zulip Mario Carneiro (Jul 19 2019 at 19:14):

Not one of our best choices

view this post on Zulip Luis Berlioz (Jul 19 2019 at 19:14):

yikes! That works.
Thanks

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jul 21 2019 at 04:18):

ask @Patrick Massot

view this post on Zulip Mario Carneiro (Jul 21 2019 at 04:20):

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


Last updated: May 11 2021 at 21:10 UTC