idris-finite-sets's Introduction

idris-finite-sets

Tools for verified finite algebra / combinatorics in Idris. Currently this is basically a port of Firsov and Uustalu's Agda library. However, I plan to add tools around finite groups and counting problems.

This software is written in Literate Idris, and intended to be both a library for Idris programs and a book for Idris programmers. For readers, familiarity with basic dependently-typed programming as covered in Type-Driven Development with Idris is assumed, along with a familiarity with the discrete mathematics commonly seen in an undergraduate introduction to the topic. But we assume no deeper familiarity with type theory or set theory.

Disclaimer and notes on public domain release

The nice thing about Idris programs is that they generally do what they say on the tin. That said, this program is full of holes (both literal and conceptual), and should not be used for anything safety-or-career-critical.

The code and text here are released under CC0, see COPYING for more information. The basic idea behind "copyright" of the code or commentary in this repository is that the set theoretic and algebraic ideas used here are considerably older than I am, and that any "original" ideas are much more a consequence of limitations in Idris and the author's own ability

That said, if you end up using this for anything serious, an acknowledgement

nicklecompte / idris-finite-sets Goto Github PK