Zulip Chat Archive

Stream: general

Topic: Notation with implicit arguments ?


view this post on Zulip 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?

view this post on Zulip 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....

view this post on Zulip 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.

view this post on Zulip 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 {  }

view this post on Zulip 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