prescientmoon/solar-conflux
1
Fork 0
Code Activity
solar-conflux/idris/learning
History
Matei Adriel 7c0fbb5f4a Make file-structures more readable
2023-10-29 01:15:32 +02:00
..
src/My Move stuff around + add lean and idris experiments 2023-10-29 00:02:10 +02:00
test Move stuff around + add lean and idris experiments 2023-10-29 00:02:10 +02:00
flake.lock Move stuff around + add lean and idris experiments 2023-10-29 00:02:10 +02:00
flake.nix Move stuff around + add lean and idris experiments 2023-10-29 00:02:10 +02:00
README.md Make file-structures more readable 2023-10-29 01:15:32 +02:00
sandbox.ipkg Move stuff around + add lean and idris experiments 2023-10-29 00:02:10 +02:00

README.md

Idris learning

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

File structure

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