👋Learning to code? Check out ourCoding Fundamentalscourse for beginners!
Join Exercism’s Idris Track for access to 56 exercises with automatic analysis of your code and personal mentoring, all 100% free.
module EvenOdd
data Even : Nat -> Type where
EZ : Even Z
ES : Even n -> Even (S (S n))
ee : Even n -> Even m -> Even (n + m)
ee EZ m = m
ee (ES n) m = ES (ee n m)
Get better at programming through fun, rewarding coding exercises that test your understanding of concepts with Exercism.
Bob is a lackadaisical teenager. In conversation, his responses are very limited.
Clean up user-entered phone numbers so that they can be sent SMS messages.
Determine if a number is an Armstrong number.
Safety first! Strong guarantees about the correctness of programs at compile time.
Inspired by lambda calculus, scopes and loops are expressed by defining and calling functions.
Categorising types into classes provides type-safe overloading.
Data being immutable allows for safer and easier-to-reason-about concurrency.
Idris supplies a small number of general-purpose features.
Idris is an actively-developed research testbed
Every language has its own way of doing things. Idris is no different. Our mentors will help you learn to think like a Idris developer and how to write idiomatic code in Idris. Once you've solved an exercise, submit it to our volunteer team, and they'll give you hints, ideas, and feedback on how to make it feel more like what you'd normally see in Idris - they'll help you discover the things you don't know that you don't know.
Learn more about mentoring
The Idris track on Exercism has 56 exercises to help you write better code. Discover new exercises as you progress and get engrossed in learning new concepts and improving the way you currently write.
See all Idris exercises
The best part, it’s 100% free for everyone.