Are there any examples of Idris that might be used to study and perhaps apply it for general purpose/"real world" application?
I am moderately proficient in Haskell, of which Idris seems to borrow significantly, and the official FAQ/documentation is rather nice but it would be very helpful to have some larger examples to explore. The goal is attempting to use Idris for practical software development. TIA.
Edwin Brady has a repo full of demos at https://github.com/edwinb/idris-demos. Among other things, it has a playable space invaders game, written using SDL bindings, Effects, and the !-effect syntax (basically an alternate syntax to do-notation / >>=).
Also, we attempt to maintain a listing of some available libraries on the wiki: https://github.com/idris-lang/Idris-dev/wiki/Libraries