idris-lang/Idris-dev — pull request #519 by reynir (2013-10-06 22:25:19+00:00)
Title: Update tutorial

- In the section about the FFI I added an emphasis on 'target'. When I was reading the tutorial I thought erroneously that 'target' was a keyword.

- I have updated (some of) the interactive proofs so they correspond to what one would see. Two proofs required an additional `compute` step.