feat(library/init/control/coroutine): add `coroutine` Remark: the termination proofs are commented because Lean 4 is currently ignoring them and accepting non-terminating functions. These files are based on an experiment implemented using Lean 3. We can find it here: https://gist.github.com/leodemoura/f5d82426c105b5fae0880e77024f6e9c We will use coroutines to implement the interaction between reader, elaborator and main driver.
Stable and nightly binary releases of Lean are available on the homepage. For building Lean from source, see the build instructions.
doxygen src/Doxyfile