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, ProcessIFace.idr, ProcessLib.idr, ProcessState.idr define it as
data ProcState = Ready | Sent | Looping
It's mildly confusing, but in the book, starting from section 15.2.3, the following definition is given:
whereas in this repo,
ProcessIFace.idr,ProcessLib.idr,ProcessState.idrdefine it as