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

feat(library/data/rat/order): use 'trans-instance' to improve performance of migrate command

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-01 08:57:10 -07:00
parent 14f7e3de94
commit 0f64a6e545
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -306,8 +306,9 @@ section migrate_algebra
zero_lt_one := zero_lt_one,
add_lt_add_left := @add_lt_add_left⦄
local attribute rat.discrete_linear_ordered_field [trans-instance]
local attribute rat.discrete_field [instance]
local attribute rat.discrete_linear_ordered_field [instance]
definition min : ℚ → ℚ → ℚ := algebra.min
definition max : ℚ → ℚ → ℚ := algebra.max
definition abs : ℚ → ℚ := algebra.abs