I don't understand why the following does not work:
Main> 2.1 + 2.3
Error: Can't find an implementation for FromDouble Integer.
(Interactive):1:1--1:4
1 | 2.1 + 2.3
^^^
It works with integers, and if I understand the docs correctly, it should work with doubles too!
I get the same error with 2.1 * 2.3, but 2.1 - 2.3 and abs 2.1 work fine, which gives me the impression that there is a problem with the Num interface. However I'm a total beginner in Idris, so maybe I'm missing something very silly! I could not find any example of summing doubles on the web…
(I compiled Idris2 from the latest commit on github — 69f680e10a336c4f33414cfd55c13d41b68d735b.)
Edited to add: 2.1 + 2.3 actually works in a file (defining a constant), the problem only occurs in the REPL. I guess I'll have to file a bug.