ternary operator

Stream: lean4

[Matthew Ballard]

I remember some discussion of the condition ? doX : doY syntax but now I cannot locate it. Am I mistaken?

[Eric Wieser]

In lean3 it existed as do tt \l condition | doY, doX...

[Adam Topaz]

Are you just looking for pythonesquejavascriptesque syntax for if _ then _ else _?

[Adam Topaz]

notation t ? p : n => if t then p else n should get you essentially all the way there.

[Matthew Ballard]

Thanks but I thought it was already somewhere in core. I might have been mistaken

[Adam Topaz]

I don't recall seeing it in lean.