From e722120e34fb9825601cf11cfa3d5e6a10084017 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Thu, 3 Sep 2015 12:22:05 -0400 Subject: [PATCH] fix(library/data/rat/order): declare decidable_le an instance --- library/data/rat/order.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean index 3ffb228165..5dedf223a7 100644 --- a/library/data/rat/order.lean +++ b/library/data/rat/order.lean @@ -321,6 +321,8 @@ section migrate_algebra attribute le.trans lt.trans lt_of_lt_of_le lt_of_le_of_lt ge.trans gt.trans gt_of_gt_of_ge gt_of_ge_of_gt [trans] + attribute decidable_le [instance] + end migrate_algebra theorem rat_of_nat_abs (a : ℤ) : abs (of_int a) = of_nat (int.nat_abs a) :=