overriding coersions

Stream: new members

[Keeley Hoek]

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)

[Floris van Doorn]

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.

[Floris van Doorn]

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

[Floris van Doorn]

(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)

[Keeley Hoek]

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