Louis Wasserman
Louis Wasserman
Work-in-progress, not ready for review, but at least putting this here to show how the parts fit together. Will complete #1353 .
It sounds like we don't necessarily want this, but I built this as a draft.
The first steps of real analysis -- certainly the first steps in the constructive real analysis developments I've seen -- involve getting basic power series up and running. What are...
I was discussing best practices with Egbert yesterday (in person!) and in particular what lessons from my background would be applicable and valuable to agda-unimath. (For context, in my professional...
In addition to the standard analytic power series in #1354 , we should consider building out the theory of formal power series and polynomials. It's not obvious to me how...
Addition of Cauchy sequences in the reals is cool and all, but we can be more general. There's nothing special about _addition_ as an operation that takes two Cauchy sequences...
I imagine we'd want an entire new folder for complex numbers. This isn't near my top priorities, but it's certainly an area we can build out, and we don't need...
I'm doing some travel with only a Chromebook that can run VSCode and at least edit Agda with all the symbols etc, but doesn't have the capacity (RAM?) to compile...
As requested in #1306 , starting a new PR for working through the docs.
I was mentioning to someone or another the difficulty of taking reciprocals of natural numbers, or doing anything significant with them, and part of the problem is that things may...