• Table of Contents
• Where is the official FAQ?
• Cabal complains about possible package breakage!
• Why isn't Idris lazy?
• Can I have lazy evaluation if I want it?
• How does the JavaScript back-end work?
• Is there some documentation for the standard lib? List of functions?
• Scraping IRC for Documentation and Comments.
• Can I do type aliases in Idris?
• Will there be support for Unicode characters for operators?
• What does Incorrect ibc version -- please rebuild warning mean?
• Where is Agda's () pattern and what is impossible?
• Can't propositional arguments be made implicit?
• Why do we have Float and Double data types? Why not Float32 and Float64?
• Why isn't there a default Cast ty ty implementation?
• Why are there both Haskell-style and GADT/Agda-style data declarations? Doesn't the latter subsume the former?
• Why does my instance declaration give the error "Can't resolve instance"?
• Does Idris work with Cygwin?
• Can I use C structs directly when binding functions through the FFI?
• Why is the module system so basic/limited?
• My proof works in the file, but not interactively. What gives?
• Where is mapM?
• Why can't I treat (->) as a function?
• Why do functions without accompanying definitions type check?
• Why do I have to use the compute tactic manually?
• What paper should I cite, if I want to reference Idris?
• Building Idris
• Cabal fails to install Idris, what could I do?
• I have installed Idris into a cabal sandbox, but where is the executable?