while let

Stream: lean4

[Reid Barton]

Is there such a thing as while let ... do (pattern match in a loop, and exit if the match fails)?

[Mario Carneiro]

No, but I don't see any reason not to. You can do it with repeat and break I think

[Mario Carneiro]

well, there is the issue that Do.lean is frozen

[Mario Carneiro]

but it might be a good idea to record it as an issue so we can come back to it later

[Reid Barton]

https://github.com/leanprover/lean4/issues/1996

[Gabriel Ebner]

You should be able to write that yourself as a macro. Expand while let pat := t do body to repeat if let pat := t then body else break