Type Driven Development with Idris requires update in Chapter 1 for Idris 2

[rjdellecese]

The "Type Driven Development with Idris: Updates Required" in the Idris 2 docs says that no changes are required for Chapter 1 (https://idris2.readthedocs.io/en/latest/typedd/typedd.html#chapter-1), but while working through Chapter 1 with Idris 2, I observed that the following expression produced an error in the REPL

Main> 2.1 * 20
Error: Can't find an implementation for FromDouble Integer.

(Interactive):1:1--1:4
 1 | 2.1 * 20
     ^^^

where the book suggests the result should look like so

Idris> 2.1 * 20
42.0 : Double

[rjdellecese]

Also, in Chapter 1 of the book:

Idris> :t Type
Type : Type 1

In my Idris 2 REPL:

Main> :t Type
Type : Type

[rjdellecese]

In 1.4.3, in attempting to run the Hello.idr program:

Main> :exec
Couldn't parse any alternatives:
1: Expected 'case', 'if', 'do', application or operator expression.

(Interactive):1:6--1:7
 1 | :exec
          ^
... (41 others)

Although this works:

Main> :exec main
Hello, Idris World!

---

And these instructions:

$ idris Hello.idr -o Hello
$ ./Hello
Hello, Idris World

Work, with the replacement of

$ ./Hello

with

$ ./build/exec/Hello

[gallais]

Are any of these not covered by https://idris2.readthedocs.io/en/latest/typedd/typedd.html ?

[rjdellecese]

All of the above are for Chapter 1, and https://idris2.readthedocs.io/en/latest/typedd/typedd.html says "No changes necessary" under the Chapter 1 header!