Lean supports coinduction, which allows you to write programs which run indefinitely. This even allows you to embed Turing-completeness, it just has to be decla

Lean supports coinduction, which allows you to write programs which run indefinitely. This even allows you to embed Turing-completeness, it just has to be declared as potentially non-terminating up-front. https://strathprints.strath.ac.uk/60166/1/McBride_LNCS2015_Turing_completeness_totally_free.pdf https://strathprints.strath.ac.uk/60166/1/McBride_LNCS2015_T...