## 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: May 11 2021 at 22:14 UTC