Idris中如何对双精度浮点数求和？REPL运算报错求助

我无法理解以下操作为何无法运行：

Main> 2.1 + 2.3
Error: Can't find an implementation for FromDouble Integer.

(Interactive):1:1--1:4
 1 | 2.1 + 2.3
     ^^^

整数运算正常，根据Idris2的Prelude.Num文档，它应该也支持双精度浮点数运算！

执行2.1 * 2.3时会出现相同错误，但2.1 - 2.3和abs 2.1可以正常运行，这让我觉得Num接口存在问题。不过我是Idris完全新手，可能忽略了一些基础内容！我在网上找不到任何双精度浮点数求和的示例……

（我从GitHub最新commit——69f680e10a336c4f33414cfd55c13d41b68d735b编译了Idris2。）

补充说明：2.1 + 2.3在文件中定义常量时可以正常运行，问题仅出现在REPL中。我想我得提交一个bug。

内容的提问来源于stack exchange，提问作者lxnv