Cleanup for the first part

[clayrat]

• made formatting consistent with latter chapters (use /idr{}, four = for exercises, etc)
• fixed some todos
• fixed some issues with functions masquerading as implicits
• replaced leb with lte
• replaced '_ with __ in hole names, as Idris's parser/ide server seems to choke on this
• replaced negb with stdlib's not, used &&/|| instead of andb/orb as much as possible
• replaced beq_nat with (==)
• removed unnecessary copies from previous chapters
• used nicer list syntax in Lists

[clayrat]

I feel like I've fixed the majority of code issues in the current develop branch. The remaining todos are mostly about editing the text and doing stylistic changes, which should probably be done separately.

[yurrriq]

:+1: to your last commit. I've actually been called into work tomorrow but I have no evening plans and will make a concerted effort to get stuff merged tomorrow night. For sanity reasons I ought not dive too deep tonight :smile:. Thanks again for absolutely crushing it lately.