difference between `if` and `match` for Bool

Stream: new members

[Asei Inoue]

def natOrString (b : Bool) : if b then Nat else String :=
  match b with
  | true => (3 : Nat)
  | false => "three"

/--
error: application type mismatch
  ite (b = true) 3
argument
  3
has type
  Nat : Type
but is expected to have type
  if b = true then Nat else String : Type
-/
#guard_msgs in
def natOrString' (b : Bool) : if b then Nat else String :=
  if b then (3 : Nat)
  else "three"

[Asei Inoue]

Why does this error occur? Why does it have to be a match?

[Damiano Testa]

I do not have a better answer than "match does more then ite", but maybe seeing how you could use ite helps:

def natOrString' (b : Bool) : if b then Nat else String :=
  if h : b then if_pos h ▸ 3
  else if_neg h ▸ "three"