Did you mean to post this on X, the everything app?
replyTry to do a web server in lean4 and we will talk after
replyhttps://github.com/emberian/dragons-net ok. or what about https://github.com/emberian/fn (runs in either lean or lisp!)
replyyeah ive never heard anyone say they like doing productive coinduction in lean. agda almost has a story, but the ergonomics and semantics arent trivial.
replythough i have thought about it.