michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/data/nat,int): make structure instances reducible

Browse source
This commit is contained in:
Jeremy Avigad 2015-01-26 12:01:19 -05:00
parent 85ef7c5151
commit 0c04c7b0d2
4 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/data/int/basic.lean
View file

@ -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

5
library/data/int/order.lean
View file

@ -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,

2
library/data/nat/comm_semiring.lean
View file

@ -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

3
library/data/nat/order.lean
View file

@ -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,