top | item 46419324

(no title)

yablak | 2 months ago

iiic the model assumes no flow control, only select.

discuss

order

amluto|2 months ago

It does. But maybe someone should prove (in Lean?) that the lack of flow control is sufficient.

Without a constraint that values aren’t ignored, the lack of flow control is certainly not sufficient, so trying to do this right would require defining (in Lean!) what an expression is.