idris-lang/idris-tutorial — pull request #29 by jfdm (2014-06-02 17:08:57+00:00)
Title: Fixed font types

Fixed font typos and removed trailing white space from lines. The latter is a side-effect of the editor.

This should address issue #27.