[bidirectional]

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_T...