14 lines
837 B
Markdown
14 lines
837 B
Markdown
# 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 |
|