Postulate, Hole, Implicit not reachable

[ysangkok]

Seems misleading to have code since they aren't used.

• IdrisImplicit isn't generated in Config.idr.
• Not sure why holes aren't getting generated, I tried ?h in a markdown snippet.
• Postulates don't seem to be generated in the compiler right now, maybe they will eventually be added, and should therefore be kept? Or have I misunderstood something? Would appreciate a test case demonstrating this.