TypeDD-Samples
TypeDD-Samples copied to clipboard
edwinb
Sample code from "Type Driven Development with Idris"
https://github.com/edwinb/TypeDD-Samples/blob/a5c08a13e6a6ec804171526aca10aae946588323/Chapter6/Printf.idr#L27 ``` Use an underscore (_) for the format, because Idris can infer from the type that it must be toFormat (unpack fmt). ``` This's the explanation from the book...
in line 91, do Just x do Display "Invalid input" Nothig -> Nothing
Since `procAdder` described in section 15.2.1 is not total, there is no need to have `Loop` constructor in `Process`. `Loop` is introduced in section 15.2.2 to make `procAdder` total, which...
It's mildly confusing, but in the book, starting from section 15.2.3, the following definition is given: ``` data ProcState = NoRequest | Sent | Complete ``` whereas in this repo,...
I am new to Idris, so forgive me if this a dumb question. When doing Exercise 5 on page 101 of the TypeDD book, my solution (which is the same...
In this example, https://github.com/edwinb/TypeDD-Samples/blob/master/Chapter2/AveMain.idr, entering ^D just cause an infinite stream of "Enter a string: The average word length is: nan". Is this expected or a bug? I expect it...
I think this ordering makes more clear that developing total state machines in idris looks something like 1. represent the state with an enumerated type (or something more complicated) 2....
