Work in process code for verified deriving of instances in Idris. Allows deriving of instances for
- Boolean Equality
- Decidable Equality
- Comparison (Ord)
- Functor
- Foldable
- Traversable Including proofs that their expected algebraic laws hold.
Work based on @ahmadsalim's MSc Thesis which was inspired by a lot of other work on generics, dependent types and levitation.
Thanks to all Contributors!