Write more idiomatic Idris

Question

yurrriq opened this issue 8 years ago · 3 comments

While this is a translation of a book written for/in Coq, we should use idiomatic Idris whenever possible.

Answer 1 · 2017-07-18T10:39:29.000Z

As a reminder, we should try replacing rewrites with dependent pattern matching where appropriate.

Answer 2 · 2017-08-03T09:57:14.000Z

This is a broader issue, but let's get it right for the first ten chapters and document some examples and lessons learned.

Answer 3 · 2017-08-03T13:46:18.000Z

Look for places where match application (http://docs.idris-lang.org/en/latest/reference/misc.html#match-application) could be introduced/used. Maybe we could fix some of the bigger replaces with it?