Zulip Chat Archive

Stream: new members

Topic: overriding coersions


view this post on Zulip Keeley Hoek (Nov 10 2018 at 13:24):

Is there a way to define a coercion which takes priority over another one? I tried @[priority 10] but it doesn't seem like it does anything to a has_coe instance (and I don't know what it should do in any case)

view this post on Zulip Floris van Doorn (Nov 10 2018 at 15:16):

Yes, that is exactly how it works. The default priority is 1000 though, so you have to make a priority higher than that to use that instance.

view this post on Zulip Floris van Doorn (Nov 10 2018 at 15:17):

Example:

set_option pp.all true
example (n : ℕ) : (n : ℤ) = int.zero := begin end
instance my_coe : has_coe ℕ ℤ := ⟨int.of_nat⟩
example (n : ℕ) : (n : ℤ) = int.zero := begin end
@[priority 500] instance my_coe2 : has_coe ℕ ℤ := ⟨int.of_nat⟩
example (n : ℕ) : (n : ℤ) = int.zero := begin end
attribute [instance] [priority 1100] int.has_coe
example (n : ℕ) : (n : ℤ) = int.zero := begin end
attribute [instance] [priority 2000] my_coe2
example (n : ℕ) : (n : ℤ) = int.zero := begin end

view this post on Zulip Floris van Doorn (Nov 10 2018 at 15:18):

(note: using attribute to change priority of a definition defined in a different file is probably bad design, because then the priority depends on whether you import that file)

view this post on Zulip Keeley Hoek (Nov 12 2018 at 08:14):

Thanks very much @Floris van Doorn , the fact that everything starts at 1000 was what I was totally missing.


Last updated: May 13 2021 at 00:41 UTC