From 0f64a6e545248433e173afb672beee2d6f3ccfd6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 1 Jul 2015 08:57:10 -0700 Subject: [PATCH] feat(library/data/rat/order): use 'trans-instance' to improve performance of migrate command --- library/data/rat/order.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean index 93e98d17b..d375c2c20 100644 --- a/library/data/rat/order.lean +++ b/library/data/rat/order.lean @@ -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