List of Listings

Chapter 1. Overview

Listing 1.1. Appending lists read from a file (pseudocode)

Listing 1.2. Hello, Idris World! (Hello.idr)

Listing 1.3. A program with a type error

Listing 1.4. Calculating a type, given a Boolean value (FCTypes.idr)

Chapter 2. Getting started with Idris

Listing 2.1. A complete Idris program to calculate average word length (Average.idr)

Listing 2.2. A function to double an Int (Double.idr)

Listing 2.3. A generic type, constrained to numeric types (Generic.idr)

Listing 2.4. Defining quadruple and rotate using a higher-order function (HOF.idr)

Listing 2.5. Local variables with let (Let_Where.idr)

Listing 2.6. Local function definitions with where (Let_Where.idr)

Listing 2.7. Calculating the average word length in a string (Average.idr)

Listing 2.8. The layout rule applied to average (Average.idr)

Listing 2.9. The layout rule, applied incorrectly

Listing 2.10. Reversing strings interactively (Reverse.idr)

Listing 2.11. Displaying average word lengths interactively (AveMain.idr)

Chapter 3. Interactive development with types

Listing 3.1. Calculating word lengths by pattern matching on the list (WordLength.idr)

Listing 3.2. Vectors: lists with lengths encoded in the type (Vectors.idr)

Listing 3.3. A skeleton definition of insSort on vectors with an initial type (VecSort.idr)

Listing 3.4. Complete definition of matrix transposition (Matrix.idr)

Chapter 4. User-defined data types

Listing 4.1. Type and data constructors from :doc