mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-11 13:36:08 +03:00
Update typedd.rst
This commit is contained in:
parent
9e84b153bd
commit
19bc230b0e
@ -19,6 +19,8 @@ necessary changes.
|
||||
Chapter 1
|
||||
---------
|
||||
|
||||
Instead of entering ``2.1 * 20``, enter ``the Double (2.1 * 20)``.
|
||||
|
||||
Instead of entering ``:exec`` to run ``Hello.idr`` in the REPL, enter ``:exec main``.
|
||||
|
||||
Chapter 2
|
||||
|
Loading…
Reference in New Issue
Block a user