Zulip Chat Archive
Stream: new members
Topic: infinite loop (on purpose)
Jason Orendorff (Aug 29 2020 at 16:52):
Suppose I wanted to write a repl in Lean. How do I make the loop?
It seems like this is possible, because I think there are some tactics that can get stuck...
Alex J. Best (Aug 29 2020 at 16:54):
Any function marked meta can recursively call itself (meta disables the termination check).
Jason Orendorff (Aug 29 2020 at 16:55):
oh sweet
Last updated: May 02 2025 at 03:31 UTC