use quotient on scheme backends

edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris

https://idris-lang.org/

Other

902 stars 58 forks source link

use quotient on scheme backends #284

Closed abailly closed 4 years ago

abailly commented 4 years ago

We compile divisions of Integers to quotient instead of '/' and add some tests for numbers, as using / has the undesirable side-effect of producing a non integral number

ziman commented 4 years ago

Related ~~(and probably conflicting)~~: https://github.com/edwinb/Idris2/pull/281

ziman commented 4 years ago

If you have a clue what's going on in https://github.com/edwinb/Idris2/pull/281#issuecomment-613673042 and how to fix it, that would be great.

abailly commented 4 years ago

@ziman Ah, did not check that PR, sorry if this PR is conflicting. I will have a look

ziman commented 4 years ago

It's actually not conflicting, as far as I can tell! It actually fixes a related issue that my PR missed.

edwinb commented 4 years ago

Thanks!