iacore

We need to discuss about the representation more. (e.g. if 7/0 is allowed in the type) (e.g. better type for equality check or simpler type (above)).

That implementation alows divided by zero. Even if we use external library, it's better to have pattern-matching for Rational numbers (and Integer too).

Sorry, should I submit a new patch? My editor gets confused by oddly indented code (indent/reindent only stop at tab break).

Sorry, but I'm not sure where I need to modify. Is there a plan to indent current codebase consistently first? As for the diff, VS Code automatically remove indent changes...

This is known as "polyfill" in browser. One way to achieve this is to import different modules depending on backend. You may have ``` foo = if __backend__ == "scheme"...

The problem is that Idris refuse compile the module again in incremental mode if it finds the same module already compiled in "whole program mode". In "whole program mode", Idris...

We should also make `idris2 --typecheck x.ipkg` only load modules mentioned. Currently it loads anything in source folder and installed folder of other packages used. The implementation should scan all...

@gallais I think this is fixed now. ``` Main> :exec putStrLn $ show "h\"a" "h\"a" ``` Is it normal for `Show String` to escape the string rather than not change...

I want to rewrite the test harness code first... why tests/Main.idr has every test's name

Here is a test case: https://github.com/locriacyber/idris2-sorted-ds/blob/05386b6f242432d21ea3ad1a6addf696b9403823/src/Data/BinaryTree.idr#L84 This should compile when the bug is fixed.