bif and do-notation

Stream: lean4

[Daniil Kisel]

bif branches don't use do-notation when the bif is inside a do block:

def main1 : IO Unit := do
  if true
    then pure ()
    else
      IO.print "a"
      IO.print "b"

def main2 : IO Unit := do
  bif true
    then pure ()
    else
      IO.print "a" -- error
      IO.print "b"

Is it as it should be?

[Eric Wieser]

An alternative suggestion: should if be notation for both cond and ite, based on the type of its argument? Then bif wouldn't exist

[Scott Morrison]

It's not ideal, but unfortunately it would be a relatively expensive feature for relatively little gain, I think.

[Mario Carneiro]

also split should work on bif