# Zulip Chat Archive

## Stream: general

### Topic: Notation with implicit arguments ?

#### Frédéric Le Roux (Jun 14 2020 at 21:01):

I would like to denote the complement of A : set X by `X \ A`

. I tried

```
notation X `\` A := @has_neg.neg (set X) _ A
```

but this has no effect, Lean still prints `-A`

. Is there a way to do this?

#### Johan Commelin (Jun 15 2020 at 05:04):

I think that the order in which notation gets declared is important... but I don't understand the system very well....

#### Floris van Doorn (Jun 15 2020 at 16:48):

I think Lean doesn't like your notation very much, since `X`

is determined by the type of `A`

.

Here is an imperfect workaround:

```
@[reducible] def my_neg (α : Type*) (s : set α) : set α := -s
notation X `\` A := my_neg X A
example (X : Type*) (A : set X) : A ∪ (X \ A) = set.univ :=
by { }
```

However, now `X \ A`

is not syntactically the same as `- A`

, so after rewriting with, say, `rw [set.union_eq_compl_compl_inter_compl]`

you will still see `- A`

.

#### Floris van Doorn (Jun 15 2020 at 16:58):

Upon further investigation, there seems to be a bug with the printing of notation declared using `@`

:

```
-- uncomment one
notation A `⁻` := set.compl A -- prints & parses correctly
-- notation A `⁻` := @set.compl _ A -- parses correctly, doesn't print
-- notation A `⁻` := @set.compl A -- parses incorrectly (as expected), but still prints!
example (X : Type) (A : set X) : A ∪ A.compl = set.univ := by { }
example (X : Type) (A : set X) : A ∪ (A⁻) = set.univ := by { }
```

#### Floris van Doorn (Jun 15 2020 at 17:02):

@Johan Commelin that order indeed matters, but you can override it with `priority`

, just as for instances:

```
notation A `¹` := set.compl A
notation A `²` := set.compl A
example (X : Type) (A : set X) : A ∪ A.compl = set.univ := by { }
notation [priority 2000] A `³` := set.compl A
notation A `⁴` := set.compl A
example (X : Type) (A : set X) : A ∪ A.compl = set.univ := by { }
```

Last updated: Dec 20 2023 at 11:08 UTC