From f3e4c734fdb2a72ec956d5f14ccce9df89acd105 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Nov 2016 16:04:40 -0800 Subject: [PATCH] fix(library/init): instance priorities --- library/init/ordered_group.lean | 4 ++++ library/init/ordered_ring.lean | 4 ++++ library/init/ring.lean | 4 ++++ 3 files changed, 12 insertions(+) diff --git a/library/init/ordered_group.lean b/library/init/ordered_group.lean index 2d4e0dc5c3..47ed260f5f 100644 --- a/library/init/ordered_group.lean +++ b/library/init/ordered_group.lean @@ -6,6 +6,10 @@ Authors: Leonardo de Moura prelude import init.group +/- Make sure instances defined in this file have lower priority than the ones + defined for concrete structures -/ +set_option default_priority 100 + universe variable u class ordered_mul_cancel_comm_monoid (α : Type u) diff --git a/library/init/ordered_ring.lean b/library/init/ordered_ring.lean index 6b53c5d348..6afbbfd7ba 100644 --- a/library/init/ordered_ring.lean +++ b/library/init/ordered_ring.lean @@ -6,6 +6,10 @@ Authors: Leonardo de Moura prelude import init.ordered_group init.ring +/- Make sure instances defined in this file have lower priority than the ones + defined for concrete structures -/ +set_option default_priority 100 + universe variable u structure ordered_semiring (α : Type u) diff --git a/library/init/ring.lean b/library/init/ring.lean index 12aee72050..03ddbe3ccf 100644 --- a/library/init/ring.lean +++ b/library/init/ring.lean @@ -6,6 +6,10 @@ Authors: Leonardo de Moura prelude import init.group +/- Make sure instances defined in this file have lower priority than the ones + defined for concrete structures -/ +set_option default_priority 100 + universe variable u class distrib (α : Type u) extends has_mul α, has_add α :=