From 0c04c7b0d256a43beb198ed675390120c98a81d0 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Mon, 26 Jan 2015 12:01:19 -0500 Subject: [PATCH] fix(library/data/nat,int): make structure instances reducible --- library/data/int/basic.lean | 2 +- library/data/int/order.lean | 5 +++-- library/data/nat/comm_semiring.lean | 2 +- library/data/nat/order.lean | 3 ++- 4 files changed, 7 insertions(+), 5 deletions(-) diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index a63a29071..1ed9d5928 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -611,7 +611,7 @@ or_of_or_of_imp_of_imp H3 section open [classes] algebra - protected definition integral_domain [instance] : algebra.integral_domain int := + protected definition integral_domain [instance] [reducible] : algebra.integral_domain int := algebra.integral_domain.mk add add.assoc zero zero_add add_zero neg add.left_inv add.comm mul mul.assoc (of_num 1) one_mul mul_one mul.left_distrib mul.right_distrib zero_ne_one mul.comm @eq_zero_or_eq_zero_of_mul_eq_zero diff --git a/library/data/int/order.lean b/library/data/int/order.lean index abe08e05f..99a7657c9 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -214,14 +214,15 @@ lt.intro section open [classes] algebra - protected definition linear_ordered_comm_ring [instance] : algebra.linear_ordered_comm_ring int := + protected definition linear_ordered_comm_ring [instance] [reducible] : + algebra.linear_ordered_comm_ring int := algebra.linear_ordered_comm_ring.mk add add.assoc zero zero_add add_zero neg add.left_inv add.comm mul mul.assoc (of_num 1) one_mul mul_one mul.left_distrib mul.right_distrib zero_ne_one le le.refl @le.trans @le.antisymm lt lt_iff_le_and_ne @add_le_add_left @mul_nonneg @mul_pos le_iff_lt_or_eq le.total mul.comm - protected definition decidable_linear_ordered_comm_ring [instance] : + protected definition decidable_linear_ordered_comm_ring [instance] [reducible] : algebra.decidable_linear_ordered_comm_ring int := ⦃algebra.decidable_linear_ordered_comm_ring, int.linear_ordered_comm_ring, diff --git a/library/data/nat/comm_semiring.lean b/library/data/nat/comm_semiring.lean index 5474db55a..2d144166a 100644 --- a/library/data/nat/comm_semiring.lean +++ b/library/data/nat/comm_semiring.lean @@ -14,7 +14,7 @@ namespace nat section open [classes] algebra - protected definition comm_semiring [instance] : algebra.comm_semiring nat := + protected definition comm_semiring [instance] [reducible] : algebra.comm_semiring nat := algebra.comm_semiring.mk add add.assoc zero zero_add add_zero add.comm mul mul.assoc (succ zero) one_mul mul_one mul.left_distrib mul.right_distrib zero_mul mul_zero (ne.symm (succ_ne_zero zero)) mul.comm diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index c5f4ff17a..2bd00f6c9 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -150,7 +150,8 @@ le.intro !zero_add section open [classes] algebra - protected definition linear_ordered_semiring [instance] : algebra.linear_ordered_semiring nat := + protected definition linear_ordered_semiring [instance] [reducible] : + algebra.linear_ordered_semiring nat := ⦃ algebra.linear_ordered_semiring, nat.comm_semiring, add_left_cancel := @add.cancel_left, add_right_cancel := @add.cancel_right,