idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.46k stars 369 forks source link

Update typedd.rst #3312

Closed m-rinaldi closed 2 weeks ago

m-rinaldi commented 2 weeks ago

Description

Entering the expression 6.0 + 3 * 12 in the REPL produces the following error on Idris 2:

Error: Can't find an implementation for FromDouble Integer.

Instead, entering the Double (6.0 + 3 * 12) behaves as stated in the book.

Should this change go in the CHANGELOG?

No

gallais commented 2 weeks ago

Btw thanks for all of these!