logoalt Hacker News

rafaelRiv • today at 3:52 PM • 3 replies • view on HN

Try to do a web server in lean4 and we will talk after


Replies

cmrx64 • today at 4:23 PM

https://github.com/emberian/dragons-net ok. or what about https://github.com/emberian/fn (runs in either lean or lisp!)

carterschonwald • today at 4:13 PM

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.