# Zulip Chat Archive

## Stream: new members

### Topic: -0

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

`theorem test : (-0:ℕ) = 0 :=sorry`

gives 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):

yes

#### 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$, 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