The documentation for repl
should read as follows:
Idris> :doc repl
Prelude.Interactive.repl : (prompt : String) ->
(onInput : String -> String) -> IO ()
A basic read-eval-print loop
Arguments:
prompt : String -- the prompt to show
onInput : String -> String -- the function to run on reading
input, returning a String to output
"words
is a vector of kStrings
" should read as
"words
is a vector of k String
s."
The reference to "section 4.2.34.2.3", should read "section 4.2.3."
In the listing at the top of the page that reads:
getEntry : (pos : Integer) -> (store : DataStore) -> (input : String)
Maybe (String, DataStore)
there should be an "->" before Maybe, i.e.:
getEntry : (pos : Integer) -> (store : DataStore) -> (input : String)
-> Maybe (String, DataStore)
"elem
follows a structure similar to decElem
" should be
"elem
follows a structure similar to isElem
."
References to the guess
function should be
to the processGuess
function.
All mentions of showItems
on this page should be listItems
.
Exercise 3 should be Exercise 5.
"This simplifies the definition of quiz
, at the cost of making the
definition of ConsoleIO
more complex"
- ConsoleIO
should be Command
.
In listing 13.1 data DoorCmd : Type
should be
data DoorCmd : Type -> Type
.
In Listing 13.4, in the line Refill : (bars : Nat)
->
the word Refill
should begin in the
same column as GetCoins
in the line above, and the :
should be aligned with the : in the line above.
In the caption for Figure 15.1, "if lines A and C are executed before lines C and D" should be "if lines A and C are executed before lines B and D."
In the program listing "Send failed"
should be
"Receive failed"
.
In listing 15.19, the last line should be: MkWCData wcount lcount
.