Formalization in Agda of the material in Analysis I, the real analysis textbook by Terence Tao.
This project depends upon the Agda standard library, as well as the agda-axiomatic library which is where many of the definitions and proofs from the textbook are actually located. Since the material is useful beyond solving textbook exercises, keeping it independent of the book's structure just made sense.
You'll need to make sure those libraries are available on your system before you can build this project's code; see Library Management in the Agda documentation for instructions.