Notation with implicit arguments ?

Stream: general

[Frédéric Le Roux]

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]

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

[Floris van Doorn]

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]

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]

@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 {  }