search

idris-hackers / software-foundations

Software Foundations in Idris
https://idris-hackers.github.io/software-foundations
MIT License
452 stars 34 forks source link

Write more idiomatic Idris #3

Open yurrriq opened 8 years ago

yurrriq commented 8 years ago

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

clayrat commented 7 years ago

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

yurrriq commented 7 years ago

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

clayrat commented 7 years ago

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?