Reid Barton (Aug 13 2020 at 13:29):
Various instances like
ring_hom.monoid : monoid (α →+* α) have the wrong priority (100) because they are defined in files with
set_option default_priority 100 at the top and don't specifically override the priority back to 1000.
Rather than go through and try to fix these all or add a linter to try to catch it, what if we add an option to Lean controlling the default priority used for instances generated by
extends, since this seems to be the main usage of setting
Reid Barton (Aug 13 2020 at 13:32):
These instances having the wrong priority is not such a big deal, but it partially defeats the purpose of lowering the instance priority of overlapping instances in the first place.
But the bigger reason for the change would be to reduce the amount of priority-related noise and especially to avoid semi-global effects like
set_option default_priority--the remaining cases where a lowered priority is needed can be handled on a per-
instance basis using
@[priority 100] instance ....
Reid Barton (Aug 13 2020 at 13:33):
The purpose of adding the option wouldn't be to modify it, rather to just make the default value 100.
Kevin Buzzard (Aug 13 2020 at 13:40):
As a dumb check right now one can look for all occurences of
default_priority in mathlib which don't have
section in the line directly above -- these are the worrisome ones
Mario Carneiro (Aug 13 2020 at 14:15):
minor quibble: it's not really
default_extends_priority but rather
extends_priority because there isn't a way to set the priority directly except after the fact AFAIK
Reid Barton (Aug 13 2020 at 14:16):
I see what you mean
Reid Barton (Aug 13 2020 at 17:41):
Last updated: May 14 2021 at 14:20 UTC