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

fix(library/data/rat): migrate for rat

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-12 04:46:34 -07:00
parent d2adf922b7
commit f25c301c98
2 changed files with 8 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -392,8 +392,10 @@ section
inv_zero := inv_zero, inv_zero := inv_zero,
has_decidable_eq := has_decidable_eq⦄ has_decidable_eq := has_decidable_eq⦄
migrate from algebra with rat definition divide (a b : rat) := algebra.divide a b
replacing sub → rat.sub definition dvd (a b : rat) := algebra.dvd a b
end
migrate from algebra with rat
replacing sub → rat.sub, divide → divide, dvd → dvd
end
end rat end rat

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

@ -222,6 +222,8 @@ section
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
migrate from algebra with rat replacing abs → abs, sign → sign
migrate from algebra with rat
replacing has_le.ge → ge, has_lt.gt → gt, sub → sub, abs → abs, sign → sign, dvd → dvd, divide → divide
end end
end rat end rat