learning-agda Just another one of my attempts to do something useful with Agda. Currently just a collection of basic numtheo proofs, but I plan to expand it into less well-traveled paths, incl. a formalization of constructive differential calculus.