👋Learning to code? Check out ourCoding Fundamentalscourse for beginners!
Join Exercism’s Idris Track for access to 57 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.
Convert a number into its corresponding raindrop sounds - Pling, Plang and Plong.
Determine if a number is perfect, abundant, or deficient based on Nicomachus' (60 - 120 CE) classification scheme for positive integers.
Create a sentence of the form "One for X, one for me.".
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 57 exercises to help you write better code.
See all Idris exercises
