Introduction to Dependent Types with Idris: Encoding Program Proofs in Types

© The Author(s), under exclusive license to APress Media, LLC, part of Springer Nature 2023

B. SitnikovskiIntroduction to Dependent Types with Idrishttps://doi.org/10.1007/978-1-4842-9259-4_5

5. Proving in Idris

Boro Sitnikovski¹  

(1)

Skopje, North Macedonia

 

This chapter provides several examples to demonstrate the power of Idris. It includes mathematical proofs. There are a lot of Idris built-ins that help you achieve your goals. Each section introduces the relevant definitions.

An information icon.Definition 1

The equality data type is roughly defined as follows:

1  data (=) : a -> b -> Type where

2  Refl : x = x

You can use the Refl value constructor ...