Negation on real numbers

[lowasser]

No description provided.

[EgbertRijke]

Awesome!

[EgbertRijke]

Some formatting needs to be edited, I'll give you a more detailed review later.

[lowasser]

I've attempted to update the formatting, PR title, etc. in accordance with what you've said elsewhere.

[EgbertRijke]

Your code looks very good! Thank you so much for all your contributions!!

[fredrik-bakke]

Very nice pull request!

[fredrik-bakke]

ah, whoops, sorry for the double up review

[EgbertRijke]

It looks like this PR just needs a make pre-commit and it has a conflict with a previous change that needs to be addressed. To do this, update your branch:

• git pull to get any changes made in the PR here on GitHub
• git pull origin master to get the changes from master. This will give merge conflicts.
• Resolve the merge conflicts
• Run make pre-commit

[EgbertRijke]

@lowasser, would you mind wrapping up this pull request when you have time?

[lowasser]

Yes, it's on my list.

[fredrik-bakke]

@EgbertRijke

Is there something wrong with our implementation of the real numbers, that we need lossy unification so much?

Now that you mention it, it likely boils down to the fact that our implementation of the rationals has to reduce fractions between every operation. Alternatively, we could follow 1lab's approach and switch to the definition of the rationals as a quotient rather than as the subtype of reduced fractions, that would probably fix this issue.

[EgbertRijke]

@EgbertRijke

Is there something wrong with our implementation of the real numbers, that we need lossy unification so much?

Now that you mention it, it likely boils down to the fact that our implementation of the rationals has to reduce fractions between every operation. Alternatively, we could follow 1lab's approach and switch to the definition of the rationals as a quotient rather than as the subtype of reduced fractions, that would probably fix this issue.

Could that really be the issue?

There's also a data definition of the rationals incoming in #1211, although I haven't done too much with that definition yet. But since it's data, it's probably fast.