Stream: new members
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 "|":
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.
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?
Mario Carneiro (Jul 21 2019 at 04:18):
ask @Patrick Massot
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