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

feat(library/data/rat): make rat subtraction reducible, fix migration of min/max

Browse source
This commit is contained in:
Rob Lewis 2015-05-26 11:52:34 +10:00
parent eb537daa1c
commit 681f431d4b
2 changed files with 10 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -309,7 +309,7 @@ infix `*` := rat.mul
prefix `-` := rat.neg prefix `-` := rat.neg
postfix `⁻¹` := rat.inv postfix `⁻¹` := rat.inv
definition sub (a b : rat) : rat := a + (-b) definition sub [reducible] (a b : rat) : rat := a + (-b)
infix `-` := rat.sub infix `-` := rat.sub
@ -426,6 +426,7 @@ section migrate_algebra
local attribute rat.discrete_field [instance] local attribute rat.discrete_field [instance]
definition divide (a b : rat) := algebra.divide a b definition divide (a b : rat) := algebra.divide a b
infix `/` := divide
definition dvd (a b : rat) := algebra.dvd a b definition dvd (a b : rat) := algebra.dvd a b
migrate from algebra with rat migrate from algebra with rat

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

@ -265,8 +265,15 @@ section migrate_algebra
definition abs (n : rat) : rat := algebra.abs n definition abs (n : rat) : rat := algebra.abs n
definition sign (n : rat) : rat := algebra.sign n definition sign (n : rat) : rat := algebra.sign n
definition max (a b : rat) : rat := algebra.max a b
definition min (a b : rat) : rat := algebra.min a b
--set_option migrate.trace true
migrate from algebra with rat migrate from algebra with rat
replacing has_le.ge → ge, has_lt.gt → gt, sub → sub, abs → abs, sign → sign, dvd → dvd, replacing has_le.ge → ge, has_lt.gt → gt, sub → sub, abs → abs, sign → sign, dvd → dvd,
divide → divide divide → divide, max → max, min → min
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]
end migrate_algebra end migrate_algebra
end rat end rat