Zulip Chat Archive

Stream: new members

Topic: -0

Alex Zhang (May 28 2021 at 08:47):

theorem test : (-0:ℕ) = 0 :=sorrygives me the error message: failed to synthesize type class instance for ⊢ has_neg ℕ. What does the error message mean? Does has_neg just mean -? (hovering over the error message does not give me any additional info)

Mario Carneiro (May 28 2021 at 08:47):


Mario Carneiro (May 28 2021 at 08:47):

the natural numbers don't have a negation

Kevin Buzzard (May 28 2021 at 08:48):

The error message means that you wrote 0-0, Lean unfolded the notation and decided that you must be using a map neg : nat -> nat and then it looked in its database (the type class inference system) and (unsurprisingly) found no such map.

Damiano Testa (May 28 2021 at 08:50):

I was also confused by something similar: the natural number do not have neg, but they do have sub.

Mario Carneiro (May 28 2021 at 08:50):

We could define such a function, but it would be very useless since -x = 0

Damiano Testa (May 28 2021 at 08:51):

So, while what you wrote does not work this does:

#check (0 - 0)
-- 0 - 0 : ℕ

Kevin Buzzard (May 28 2021 at 08:51):

@Alex Zhang has_neg is a "notational typeclass", the simplest kind of typeclass. If you have any random term a of any type X, and you write -a, then Lean tries to find a so-called "instance" of has_neg X, which in practice means that it looks through all the stuff which has been imported and sees if anyone has defined a map neg : X -> X and told this map to the system using the instance command. You can read about classes and instances in chapter 10 of #tpil

Kevin Buzzard (May 28 2021 at 08:53):

The reason for this is the following two lines right at the beginning of core Lean 3:

class has_neg      (α : Type u) := (neg : α  α)
prefix -       := has_neg.neg

The first line makes the has_neg class, the second line attaches the notation - to the class.

Kevin Buzzard (May 28 2021 at 08:54):

def X := 

def X.neg : X  X := λ x, (37 : )

instance : has_neg X :=
{ neg := X.neg }

variable (x : X)

#check -x -- works

Kevin Buzzard (May 28 2021 at 08:55):

If you remove the instance line you'll get the same error as the one you were facing with nat.

Last updated: Dec 20 2023 at 11:08 UTC