A brief example-based introduction to Idris, originally for a Mini-Workshop held by the the [Programming Languages and Software Technology Group][PS] at the University of Marburg.
Idris is a hip new functional programming language with dependent types. In this talk I will give a whirlwind tour of some features that make Idris interesting and fun to use, including: typed laziness, data and codata, interactive tactic-based theorem proving, extensible syntax, and a library-level effects system.