Reid Barton
Reid Barton
I think the new comment might be a bit easier to read if you swap the two Haskell bits; then it reads more like a definition of ``, which is...
Yes, exactly.
I noticed this too while preparing a patch to provide `tcdrain()` on Android—a function whose _only_ purpose is to block! The plan above sounds reasonable to me.
Another +1. I've built GHCi for Android with some modifications to the script, but am now wondering about the licensing situation.
@bendlas, I'm lost, how do you expect this to work? Are you running GHC on an ARM system? If not, how do you expect to link in ARM object files,...
- `isinstance` checks that will always return True or always return False probably indicate a mistake (in the latter case we have to assume no multiple inheritance).
I think we absolutely should implement a ("verifying") computer algebra system in Lean. I'm not sure whether it is better to do it now, or wait for Lean 4. I'm...
I'm a bit confused: is the `has_pow` instance changing (up to defeq) or not? If so then why?
Yes, I think it is definitely better to have a useful definition of `^` than to save a few lines in the internals of `real`.
I suggest we abandon this given that it seems to work better in Lean 4 to use a CommRing instance like the present mathlib 3 one.