|
|
|
|
|
by neel_k
3297 days ago
|
|
> I hear "dependent types" and I think "theorem prover", but it seems like Idris is a cleaned up Haskell with some light proving features built in? It's a full-strength dependent type theory, but is intended primarily for use as a programming language. So the design focus is on using full dependent types to make ordinary programming easier. > What's a good excuse to try Idris? The best excuse of all: it is super fun. |
|