Try to do a web server in lean4 and we will talk after
https://github.com/emberian/dragons-net ok. or what about https://github.com/emberian/fn (runs in either lean or lisp!)
yeah ive never heard anyone say they like doing productive coinduction in lean. agda almost has a story, but the ergonomics and semantics arent trivial.
though i have thought about it.
https://lean-lang.org/doc/api/Std/Http/Server.html
https://leangineer.com/blog/realworld-in-lean/
https://news.ycombinator.com/item?id=50088748