Browse the Agda code in HTML here.
- Custom entrypoint with all basic imports in
Prelude.Init
- General properties of standard types in
Prelude.General
- Metaprogramming utilities in
Prelude.Generics
- Typeclasses:
- Default/ToN/Show/DecEq/Measurable/Collections
- Functor/Bifunctor/PointedFunctor/Applicative/Monad/Semigroup/Monoid/Nary
- List utilities
- Abstract APIs for Sets/Maps
- Utilities for cryptography, unsafe operations and working with irrelevance