# Idris learning

This directory contains the results of my first adventure into the world of Idris 2.

## File structure

| File                                              | Description                                   |
| ------------------------------------------------- | --------------------------------------------- |
| [Nats.idr](./src/My/Nats.idr)                     | Natural numbers                               |
| [Signs.idr](./src/My/Signs.idr)                   | Signs (essentially $\mathbb Z / 2 \mathbb Z$) |
| [Integers.idr](./src/My/Integers.idr)             | Integers as differences of naturals           |
| [Structures.idr](./src/My/Structures.idr)         | Setoids, semigroups, monoids and groups       |
| [Syntax/Rewrite.idr](./src/My/Syntax/Rewrite.idr) | Coping with the lack of tactics               |