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

fix(library/data/rat/order): declare decidable_le an instance

Browse source
This commit is contained in:
Rob Lewis 2015-09-03 12:22:05 -04:00 committed by Leonardo de Moura
parent 7c966e3d02
commit e722120e34
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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) :=