mathlib3
4b6fcd90
- perf(data/gaussian_int): speed up div and mod (#1394)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
6 years ago
perf(data/gaussian_int): speed up div and mod (#1394) avoid using `int.cast`, and use `rat.of_int`. This sped up `#eval (⟨1414,152⟩ : gaussian_int) % ⟨123,456⟩` from about 5 seconds to 2 milliseconds
References
#1394 - perf(data/gaussian_int): speed up div and mod
Author
ChrisHughes24
Committer
mergify[bot]
Parents
974d413b
Loading